Custom Query (361 matches)

See Pure/ProofGeneral?/parsing.ML.

This is an absolutely essential improvement required for Isabelle2007 to have good PGIP support.

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> 

[Reported by Michaël Cadilhac]

I'm an Emacs22 user of Proof General, and I experienced some bugs with buffer-invisibility-spec on several occasions.

In GNU Emacs 22.0.93.6 (i686-pc-linux-gnu, X toolkit, Xaw3d scroll bars)
 of 2007-02-09 on mistral
X server distributor `The X.Org Foundation', version 11.0.70101000
configured using `configure  '--prefix=/usr' 'CFLAGS=-O0 -ggdb''

The problem arose when buffer-invisibility-spec was of the form ((smthg . t) t).

Note, I don't know if the patch breaks something with XEmacs. Maybe the following functions aren't defined:

(defun add-to-invisibility-spec (element)
  "Add ELEMENT to `buffer-invisibility-spec'.
See documentation for `buffer-invisibility-spec' for the kind of elements
that can be added."
  (if (eq buffer-invisibility-spec t)
      (setq buffer-invisibility-spec (list t)))
  (setq buffer-invisibility-spec
	(cons element buffer-invisibility-spec)))

(defun remove-from-invisibility-spec (element)
  "Remove ELEMENT from `buffer-invisibility-spec'."
  (if (consp buffer-invisibility-spec)
    (setq buffer-invisibility-spec (delete element buffer-invisibility-spec))))