[isabelle-dev] exception XML_BODY with Simpl in recent jEdit
makarius at sketis.net
Wed Oct 3 18:10:42 CEST 2012
On Wed, 3 Oct 2012, Makarius wrote:
>> Defining statespace "foo_parameters" ...
>> Defining statespace "foo_variables" ...
>> exception XML_BODY [<xml_elem xml_name="typing"><xml_body>char list =>
>> ('f, 'g, 'h) com option</xml_body>\<Gamma></xml_elem>,
>> , <xml_elem xml_name="typing"><xml_body>char
>> list</xml_body>foo_'proc</xml_elem>, = Some foo_body.foo_body] raised
>> (line 384 of "PIDE/xml.ML")
Using Isabelle/74ad6ecf2af2 it should work with both of the following AFP
date: Wed Oct 03 17:48:48 2012 +0200
more robust print_term, which is inherenty fragile;
date: Wed Oct 03 18:02:21 2012 +0200
more systematic term-as-string embedding via YXML -- NB: types seem to be
not precise here and are better stripped beforehand;
There is a funny historic story behind it: When Norbert Schirmer made this
locale version of Simpl, there was still no proper ML interface for it, so
he turned terms into strings, to be processed again by the system in the
well-known fragile way. Some months later, locales did acquire ML
interfaces, but Simpl was not updated -- which was not so unexpected.
Some years later (2011) I provided some YXML backdoors to sneak full terms
into string interfaces in a more systematic manner; this now helps out in
the above situation as well and hopefully lasts longer.
More information about the isabelle-dev