On 05/23/2012 10:38 PM, Makarius wrote:
On Wed, 23 May 2012, Christian Sternagel wrote:

3) Furthermore, in my course I recommend students (which know about
term rewriting before) to have a look at the simplifier trace whenever
the simplifier does something unexpected or does not terminate.
However, for the latter use-case (i.e., finding cause of
nontermination) I do not even know how to do it myself in jedit. As
soon as I write, e.g., "apply simp" the simplifier starts to loop, if
I don't delete the command it continues looping (and thus the whole
system becomes highly unresponsive very soon), if I delete the
command, the trace is gone too. Is there any way (or workaround), such
that I can generate (part of) the trace of a (potentially) looping

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. 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). (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).


isabelle-dev mailing list

Reply via email to