[isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
makarius at sketis.net
Sun Sep 18 17:10:50 CEST 2011
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.
More information about the isabelle-dev