[isabelle-dev] NEWS: Isabelle/jEdit (19e1c6e922b6)
noschinl at in.tum.de
Tue Sep 13 11:38:22 CEST 2011
On 06.09.2011 21:58, Makarius wrote:
> * Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
> "isabelle jedit" on the command line.
> . Management of multiple theory files directly from the editor
> buffer store -- bypassing the file-system (no requirement to save
> files for checking).
Nice! Together with the improved scheduling, I was able to use
Isabelle/jEdit for some serious work (tuning the simpset for
In the beginning I was irritated when Isabelle/jEdit complained about
missing theory files, when the files where obviously there (and loaded).
Later I found out, that this error is also displayed if there are any
errors (transitively) in these theory files.
> . Markup of formal entities within the text buffer, with semantic
> highlighting, tooltips and hyperlinks to jump to defining source
> . Refined scheduling of proof checking and printing of results,
> based on interactive editor view. (Note: jEdit folding and
> narrowing allows to restrict buffer perspectives explicitly.)
When looking at simplifier traces, if found the output display not
really smooth yet, sometimes I had to move the cursor a bit around, till
the output view displayed what I expected; but I have not analyzed yet,
what exactly goes "wrong".
> . Reduced CPU performance requirements, usable on machines with few
> . Reduced memory requirements due to pruning of unused document
> versions (garbage collection).
As some data point: I was able to load HOL/Probability/Probability.thy
(using HOL-Image), but needed my whole memory for this (6GiB).
Pruning unused document versions sometimes interferes with the option to
_not_ update the output window automatically: To compare the effect of
different simpsets, I added a new output window and unchecked the "auto
update" option. Then I changed the simp call and the not-updating output
window went blank.
> See also ~~/src/Tools/jEdit/README.html for further information,
> including some remaining limitations.
Some further comments:
- The command line help shows some option "-l" to use a different
logic image, but this does not seem to work.
- 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. I can try to reproduce it, if you are
More information about the isabelle-dev