[isabelle-dev] simplifier trace (and jedit)

[Makarius]

On Thu, 24 May 2012, Christian Sternagel wrote:

>> The Prover Session panel has check/cancel buttons that are reminiscent 
>> of manual control in PG. The keyboard shortcuts are C-SPACE and 
>> C-BACKSPACE, respectively. You need to avoid rash movements after 
>> cancelation, outerwise the checking process restarts.

> I overlooked those, thanks! Unfortunately, this does not work very well 
> (or maybe I misunderstood the intended way of use). I don't see the 
> purpose of "Check", since it seems that as soon as I start typing again, 
> asynchronous checking does start anyway.

Normally the implicit execution process follows the "perspective" of the 
editor, i.e. the set of visible text ranges.  So when you move around and 
expose more text, it causes updates on the perspective (edits) and 
eventual checking.

The "Check" button or C-SPACE key pretends that the whole buffer is 
visible, and thus commences its full checking until you change the 
perspective again.

Eventually, I would like to make this yet more declarative, with some 
properties to control the checking process of the session, say to assert 
that a certain subgraph of the current session is processed continously.


> While clicking on "Cancel" does not always cancel the process (or maybe 
> there is just a huge delay, since the trace is so big; anyway the result 
> is that jedit becomes unresponsive and I basically have to kill it).

This could well be.  The protocol is asynchronous and maximizes 
throughput, without any flow control.  So the prover can easily cause 
denial-of-service of the front-end side.

After all these years with this fundamental problem of high-volume traces, 
I think I now know how to avoid it in the first place.  The idea is to 
"pause" prover transactions in certain situations, say after a certain 
amount of tracing messages have been output.  The user then needs to react 
on it, by clicking somewhere in the Output window, or entering some text 
in an input field.

This could work via Future.promise/fulfill in a similar way like the 
Invoke_Scala.method function in Isabelle/ML.  This works, because the 
documen model is inherently multi-threaded.


> The keyboard shortcuts do not work for me, C-SPACE is already in use in 
> my GNOME, so I know why this does not work, but C-BACKSPACE apparently 
> does backwards deletion of a word inside jedit; I'll check whether this 
> works when I set different keyboard shortcuts).

It is C-E SPACE and C-E BACKSPACE, and a bit too close to 
ESCAPE-META-ALT-CONTROL-SHIFT.  C-E is a common jEdit prefix for certain 
"extended" key sequences.

See also the jEdit "Shortcuts" options in the "Plugin: Isabelle" section.


 	Makarius