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