Custom Query (361 matches)

XEmacs 21.4.21 on Ubuntu Linux 8.04; Isabelle2008.

The special markup (for terms etc.) is not processed in minibuffer messages. For example:

ML_command {* warning (Syntax.string_of_typ @{context} @{typ 'a}) *}

Here the decoration for 'a shows up as funny control characters, instead of proper font-lock colouring.

Proof general starts correctly with emacs but when I try to start coq with C-c C-s I get a

Symbol's value as variable is void: dir

the trace is

Loading /Users/ryan/emacs/ProofGeneral-3.7.1pre080526/ProofGeneral/generic/proof-toolbar.el (source)...done Loading /Users/ryan/emacs/ProofGeneral-3.7.1pre080526/ProofGeneral/generic/pg-user.el (source)...done Loading /Users/ryan/emacs/ProofGeneral-3.7.1pre080526/ProofGeneral/generic/proof-shell.el (source)...done Loading /Users/ryan/emacs/ProofGeneral-3.7.1pre080526/ProofGeneral/generic/proof-x-symbol.el (source)...done file-exists-p: Symbol's value as variable is void: dir [2 times]

I'm using these versions, although this same behavior happens with the stable version of Proof General and with Coq 8.1pl2:

This is GNU Emacs 22.1.1 (i386-apple-darwin9.2.2, Carbon Version 1.6.0)

The Coq Proof Assistant, version 8.1pl3 (Dec. 2007)

Version 3.7.1pre080526

In the *response* buffer the cursor is not visible, but can be moved as expected.