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.

isabelle-dev mailing list

Reply via email to