Custom Query (361 matches)

When using "Extraction Library <Module>", the "Library" word is not highlighted in blue like all other keywords (Extraction, Require, etc).

I can now get most symbols displayed by choosing "Apple Symbols" in the Tokens menu with the exception of symbols in antiquotations like @{term "\<Longrightarrow>"}. For these I need to commit to "Apple Symbols" for the whole buffer, from the Options > Appearance menue (which works with pre110131).

This is GNU Emacs 23.x on Linux or Mac OS.

The default proof-full-annotation uses a lot of resources, both on the Emacs and ML side, resulting in odd instabilities.

For example, open the file Isabelle2011/src/HOL/Auth/Message.thy and assert the whole buffer. This is quite slow, and there is a good chance that it stops in the middle with an Interrupt from the prover (which indicates some low-memory situation).

For this reason, the distributed Proof General is patched to have proof-full-annotation disabled by default.