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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
