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

[Lars Noschinski]

Hi,

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).

   -- Lars