Custom Query (361 matches)

The current undo management code uses a long history of commands sent to the prover, then weeds through them to figure out which commands need undoing and how. This is tedious and will not support context switching. Currently there is no queue of undo commands but instead a thread is made for each undo command as one-by-one they are processed by the prover; this has very poor performance.

The document itself has exactly the information needed to calculate undo commands, based on the processed position. Because the document locks the processed text, this is expected to be accurate. We can calculate a queue of commands for undoing just as we do when processing commands.

This work has begun but amounts to a major reorganisation/extension of the document model. This ticket will be used to track progress.

The current Isabelle CVS version displays goals correctly but double-escapes the XML in terms when it prints theorems.

Test case: run isabelle -I -X and paste in the following two PGIP lines:

<pgip class="pa" id="test" seq="1"><opentheory thyname="SymbolOutput" parentnames="Main">theory SymbolOutput imports Main
begin</opentheory></pgip>

<pgip class="pa" id="test" seq="2"><spuriouscmd>thm trancl_def</spuriouscmd></pgip>

the output should contain text like this:

<pgmltext>trancl <sym name="equiv">&lt;equiv;&gt;</sym>;equiv;&gt;</sym>

and not text like this:

<pgmltext>trancl &lt;sym name = &quot;equiv&quot;&gt;\&amp;lt;equiv&amp;gt;&lt;/sym&gt;

which has too much escaping. The goals output does the right thing, e.g. try this PGIP command:

<pgip class="pa" id="test" seq="3"><opengoal>lemma "P \&lt;equiv&gt; P"</opengoal></pgip>

which gives PGML text containing:

goal (1 subgoal):
 1. <atom kind = "free">P</atom> <sym name = "equiv">\&lt;equiv&gt;</sym> 

Editing document sets the parse edit offset, the position from which parsing begins next time.

The code for adjusting this had faulty logic in earlier versions. It was fixed but seems to have broken again, perhaps with parser adjustments. This causes bad breakage because it gets difficult to edit text.