Custom Query (361 matches)

Indentation is not closed properly after an "Abort." statement, following "Theorem".

Simple fix: In coq/coq-syntax.el: Add "Abort" to the list of keywords defined in coq-keywords-save-strict (line 618 in ProofGeneral-3.7pre071025).

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.

Isabelle fails to start up with PG 3.7 and XEmacs 21.5.28, not sure if this is intended to work.

I have attached the error trace.

The same / a similar issues was also reported on the Isabelle mailing list, cf.:

​https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2007-August/msg00065.html