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

[Lars Noschinski]

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

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
> positions.
>
> . 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
> cores.
>
> . 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
     interested.

   -- Lars