[isabelle] export and import term



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
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.