[isabelle-dev] jedit interface

Makarius makarius at sketis.net
Mon Sep 23 14:55:54 CEST 2013


On Thu, 19 Sep 2013, Makarius wrote:

> On Wed, 18 Sep 2013, Tobias Nipkow wrote:
>
>> I just noticed the following behaviour in 705f0b728b1b: When the cursor 
>> remains
>> fixed in the theory window and I scroll in that window with the help of the
>> scoll bar, the output window goes blank when the line with the cursor is no
>> longer visible. I have no idea when that changed but in Isabelle 2013 it 
>> was not
>> like that - the output would not go blank.
>
> I think it is just a consequence of the major reforms of the document 
> execution model from this summer.  Since this is my own department it will be 
> easy to address, and not require descending into the dungeons of JDK sources 
> again.  I will come back to this within a few days.

changeset:   53780:ef62204a126b
user:        wenzelm
date:        Sat Sep 21 20:58:32 2013 +0200
files:       src/Tools/jEdit/src/document_view.scala
description:
caret range of active text area counts as visible (e.g. relevant for 
Output after scrolling outside of text view);


It remains to be seen if this is exactly the right notion of visibility to 
get Output of proof states as expected in most situations.

The point here is that the system gives up old prover output when it is 
considered unreachable by GUI components.  This conserves scarce JVM 
memory resources (see also d598b6231ff7).


 	Makarius



More information about the isabelle-dev mailing list