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

[Makarius]

On Wed, 3 Oct 2012, Lars Noschinski wrote:

> I noticed a problem with jEdit in Isabelle 1cf810b8f600 and Simpl from AFP 
> 8185fe753fa9: Consider the following example theory.
>
> --------------------------
> theory Scratch imports Vcg begin
>
> procedures foo (I :: bool | O :: bool) "SKIP"
>
> end
> --------------------------
>
> The procedures line produces the following output:
>
> 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")
>
> This error does not occur in Isabelle 2012 and it also did not occur before 
> my vacation, i.e. with an repository version of around 3 weeks ago (is there 
> a way to see the version id from before the last pull? In git, I could this 
> information from the reflog).

For me it suffices to know just one point in the relevant histories.  I 
will take a look shortly.


 	Makarius