[isabelle-dev] exception XML_BODY with Simpl in recent jEdit

[Makarius]

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 
changes:

changeset:   3074:585c253aac21
user:        wenzelm
date:        Wed Oct 03 17:48:48 2012 +0200
files:       thys/Simpl/hoare.ML
description:
more robust print_term, which is inherenty fragile;


changeset:   3075:6d517c0cb09e
user:        wenzelm
date:        Wed Oct 03 18:02:21 2012 +0200
files:       thys/Simpl/hoare.ML
description:
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.


 	Makarius