#84 closed defect (fixed)
Remove double-quoted XML output from term display
Reported by: | David Aspinall | Owned by: | David Aspinall |
---|---|---|---|
Priority: | blocker | Milestone: | |
Component: | 4:prover-isabelle | Keywords: | |
Cc: |
Description
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"><equiv;></sym>;equiv;></sym>
and not text like this:
<pgmltext>trancl <sym name = "equiv">\&lt;equiv&gt;</sym>
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 \<equiv> P"</opengoal></pgip>
which gives PGML text containing:
goal (1 subgoal): 1. <atom kind = "free">P</atom> <sym name = "equiv">\<equiv></sym>
Change History (3)
comment:1 Changed 17 years ago by
comment:2 Changed 17 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
To see the output exactly as shown above you need to turn on symbol output with the
<sym>
element:however, the output after the first command still shows the problem because the
<atom>
elements are wrongly quoted as<atom kind = "
etc.