[isabelle-dev] jEdit: re-checking of main buffer

[Makarius]

On Sat, 31 Aug 2013, Christian Sternagel wrote:

> Assuming that the grayish background highlighting really indicates 
> prover activity in the background

This is outdated_color (RGB=EEE3E3 by default).  It means that the 
asynchronous protocol is in an intermediate state where the editor has no 
confirmation from the prover about the last round of updates yet.

The prover needs to update certain internal administrative structures of 
the document model until this confirmation ("the assignment") can be given 
back to the editor.  This requires usually a few milliseconds, but depends 
on availability of CPU resources, and can get into the range of 0.5..2 
seconds.  (What are your hardware parameters?)

Until recently (notably in Isabelle2013) these "update -- assign" cycles 
of the document model involved explicit cancellation of all running 
executions of the prover *before* doing anything.  There was a restart of 
transactions that were still needed in the next document version.  This 
was OK for the majority of quick proof commands, but noticable for slow 
things like 'fun' or heavy proof tools.  With the integration of 
sledgehammer etc. into the document model, the end of this approach was 
come: accidental cancellation and restart of big ATP jobs was not 
feasible.


So I reworked the whole approach quite substantially.  As a consequence 
the prover never stops, it merely refrains from starting new tasks. Then 
edits are applied "on-line" and old tasks are cancelled afterwards if they 
are no longer needed.

This means that there are fewer CPU resources available for doing the 
administrative update of document content.  Often it is just the protocol 
thread itself, which pretends to be another worker thread for this purpose 
(this guarantees progress, but a fully saturated worker farm might still 
work against it).

For my part, I've seen the change in behaviour and got used to it after a 
few days. It is just a matter of tradeoff between seeing more "outdated" 
text views vs. long-running tools continuing all the time undisturbed. I 
am not aware of a genuine problem -- if there is one you should report 
that again.


> I recently noticed that sometimes a "re-check" of the whole buffer

An actual "re-check" would be something else: new "execs" assigned to 
existing command transactions, involving a change to pink and purple etc. 
This should not happen here, unless there is something wrong in the 
implementation.

In fact the new strictly monotonic model should involve fewer "re-checks". 
In the past, a long-running proof step upwards in the buffer could cause a 
reset to that position with a fresh start of everything in between.


> when I select the second "by auto" (typically S+Home, since the courser 
> is positioned directly behind it after just having typed it) and then 
> replace the selected region by something different, the whole buffer is 
> highlighted (thus re-chekced or re-parsed?).

"Re-parsed" is yet another thing: whenever you do some physical edits on 
the buffer, Isabelle/Scala will check on its side if anything has 
structurally changed to tell the prover about it.  This requires some JVM 
resources, but it should not be visible in the editing process.  Vacous 
updates in that respect are ignored.

On the other hand, just scrolling around is a full update of the document 
model, and might cause brief appearance of the "outdated" color scheme. 
This is particularly relevant to the new "print functions" and "query 
operations" of the document model.  Uncovering parts of the text might 
cause the prover to do anything from plain 'print_state' to 'sledgehammer' 
(in its "auto" mode).


 	Makarius