Custom Query (361 matches)

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.

I'm just trying to get ProofGeneral to work with XEmacs 21.5.28 and Fedora Linux. During startup, I get a long and unreadable error message starting with something like

(1) (file-mode-spec/warning) Error in File mode specification: Wrong type argument: consp, latin-iso8859-2 

I noticed this problem while I was visiting a user who is using Fedora release 7 (Moonshine), Kernel 2.6.23.1-21-fc7 on an i686. However, I also had the same problem on one of our machines at TUM, running XEmacs 21.5.28 and openSUSE 10.3.

PG-Emacs: 3.7pre071112 Isabelle: 2007

Here is a reproducible way to get ProofGeneral 3.7pre071112 out of sync with the isabelle2007 process, simply process this theory:

theory Scratch imports Main begin

lemma X: "a=b ==> b=a" by simp -- "Text with \illegal escape sequence"

end

This happens quite often if you insert latex in your formal comment and forget to convert "..." to {*...*} syntax. Having to restart Isabelle each time is annoying for large theories.