Email Gateway (Aug 19 2022 at 11:06): Email Gateway (Aug 19 2022 at 11:06):From: Yuhui Lin <Y.H.Lin-2@sms.ed.ac.uk>
Hi,
I've got a an exception "exception XML_ATOM term raised" when I use Syntax.parse_term to parse a string which is exported by Syntax.string_of_term, e.g.
Syntax.string_of_term @{context} @{term" a + b"} |> Syntax.parse_term @{context};
The reason for me to do this is that the system, which I am developing, need to communicate with Isabelle. So I want to export and import terms in Isabelle as string to my system in the json format in ML. But I get the above exception. Where do I go wrong here ? Thanks in advance.
best,
Yuhui
Email Gateway (Aug 19 2022 at 11:06):From: Makarius <makarius@sketis.net>
On Wed, 15 May 2013, Yuhui Lin wrote:
I've got a an exception "exception XML_ATOM term raised" when I use
Syntax.parse_term to parse a string which is exported by
Syntax.string_of_term, e.g.Syntax.string_of_term @{context} @{term" a + b"} |> Syntax.parse_term
@{context};
Conceptually, functions like Syntax.string_of_term from Isabelle inner
syntax produce a pretty tree with additional markup. Its main purpose is
to be output via one of the standard Isabelle channels (writeln, warning
etc.), e.g. like this:
ML {*
val s = Syntax.string_of_term @{context} @{term" a + b"};
writeln s;
*}
The front-end on the Isabelle/Scala side then renders the pretty tree as
best as it can -- Isabelle/jEdit presently uses a lot of this information
for hilighting, hyperlinks, tooltips etc.
You can peek at that raw XML tree representation in Isabelle/ML using
YXML.parse_body on the string s above. This is mainly for information,
normally you don't work with these internal representations directly.
There are some tricks to avoid producing extra markup, and get back to
nostalgic raw text output, but one should try first to stay within the
regular mode of operation. Note that Syntax.parse_term cannot recover
exactly the same term in general, even when printed without YXML markup.
The reason for me to do this is that the system, which I am developing,
need to communicate with Isabelle. So I want to export and import terms
in Isabelle as string to my system in the json format in ML. But I get
the above exception.
There are various ways to do that, depending what you actually need.
For example, you can use encode/decode functions from the XML and Term_XML
module (both in Isabelle/ML and Isabelle/Scala) to get structured values
back and forth, without concrete syntax getting in between.
The Isabelle term parser also accepts low-level YXML terms directly like
this:
ML {*
val t = @{term "a + b"};
val yxml = YXML.string_of_body (Term_XML.Encode.term t);
writeln (YXML.embed_controls yxml);
*}
Now the Output panel in Isabelle/jEdit shows some funny string with bold X
and Y characters. This is you externalized term, it can be sent around
between process, over the Net etc.
It can be re-internalized in Isabelle/Isar, e.g. like this:
term "XY5XXY:..."
The same in Isabelle/ML:
ML {*
val t' = Term_XML.Decode.term (YXML.parse_body yxml);
@{assert} (t = t');
*}
Thus you can bypass traditional troubles with official "XML", even json.
Note that Isabelle/Scala hardly provides any operations on logical Term
language.
Makarius
Last updated: Apr 25 2024 at 04:18 UTC