[isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)

[Makarius]

On Tue, 13 Sep 2011, Lars Noschinski wrote:

> Is Isabelle/jEdit supposed to work with Pure as a logic image? On
> one occasion, it misparsed a document because it did not consider
> datatype as a keyword.

Yes, but it is a bit difficult to load a session from there that defines 
many commands, like main HOL.  The problem is that the command/keyword 
table is still a global state variable of the session that is implicitly 
updated in an erratic manner.  This is incompatible with the organisation 
of parsing and evaluation of commands within PIDE documents.

You can carefully "Reload" the first theory node that has crashed after 
redefining a command, and continue slowly outwards in the theory 
dependency graph.  This is a bit tricky due to absence of graph 
visualization, but in Isabelle/a04f3eb3943c the "Prover Session / Theory 
Status" panel shows a topologically ordered list, at the least.


 	Makarius