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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
