Remove double-quoted XML output from term display

[David Aspinall]

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> 

[David Aspinall]

To see the output exactly as shown above you need to turn on symbol output with the <sym> element:

<pgip class="pa" id="test" seq="1"><pgmlsymbolson/></pgip>

however, the output after the first command still shows the problem because the <atom> elements are wrongly quoted as <atom kind = " etc.

[David Aspinall]

Milestone PG-Eclipse-1.0.6 deleted