Custom Query (361 matches)

I'm glad to see that support for finding the lisp files relative to the "proofgeneral" script has been added in the CVS Proof General; I had hacked such a feature into my own copy of Proof General 3.7.1. But the feature is broken in two ways:

• It sets PGHOME to the "generic" subdirectory instead of the main "ProofGeneral" directory.

• It is actually looking relative to the working directory. It should look relative to the script ($0) so that the user can start it with the working directory set to any desired directory containing files the user wants to edit.

The attached patch fixes it.

The font-lock setup does not handle \<^sub> and \<^sub> properly if X-Symbol mode is enabled only later via the menu. For example, in Isabelle/HOL

  thm wf_trancl

displays \<^sup> verbatim. If the printed text is pasted into the source buffer it is shown properly as superscript. It also works as expected if X-Symbol is enabled right from the start, using option -x true.

Using GNU emacs 22.1.1 on Ubuntu 7.10, the editor occasionally hangs when doing isearch-forward.

E.g. reproduce this by visiting Isabelle/src/HOL/Lambda/WeakNorm.thy: type C-s, type "c" "o" "n" "s" (which finds an occurreny of "Cons" in the text), continuing to type "t" makes emacs hang; after C-g it works again, but there is some danger it will again hang later.