diff options
| -rw-r--r-- | BUGS | 6 | ||||
| -rw-r--r-- | CHANGES | 2 | ||||
| -rw-r--r-- | etc/announce | 2 | ||||
| -rw-r--r-- | todo | 8 |
4 files changed, 16 insertions, 2 deletions
@@ -15,6 +15,12 @@ versions, and those which only apply to particular versions. * Generic problems, for all Emacs versions +** X-Symbol support removed from "secondary" provers (HOL, ACL2, LEGO, Twelf) + +If anyone was actually using this, please let me know. It should be +very easy to revive by copying coq/x-symbol-coq.el (although a generic +version might be desirable). + ** Visibility control doesn't distinguish theorems with same name. If you have more than one theorem with the same name in a buffer, @@ -204,7 +204,7 @@ APIs), then you may have to upgrade your Isabelle version as well. ** Changes for Coq -*** Indentation +*** Indentation improved *** Menu entries for commands, tactics and terms diff --git a/etc/announce b/etc/announce index a8d1aa31..5a28a99b 100644 --- a/etc/announce +++ b/etc/announce @@ -7,7 +7,7 @@ Proof General is a generic (X)Emacs interface for proof assistants. It can be instantiated for the proof assistant of your choice, and is supplied ready-customised for Isabelle, Coq, LEGO, and PhoX, and, -experimentally, for HOL98, Twelf, and ACL2. +experimentally, several other systems. Proof General includes these features, amongst others: @@ -95,6 +95,14 @@ X (Low) e.g. probably not worth spending time on *** PGIP SUPPORT (minimal for Isabelle patch): -- settings with categories +*** A Oddity: Weirdness with regions turning blue even though they + haven't been processed. Noticed with HOL/CCC experimental setups. + Send a few regions queueing, no result from interpreter, yet sometimes + turns blue. Why??? + +*** Allow empty retract action that doesn't produce new prompt + (Noticed with HOL4). + *** [ Don't query save before retraction ?? ] *** C Implement optional arg to next/undo which doesn't update |