diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-14 16:30:28 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-14 16:30:28 +0000 |
| commit | c621a2ea58e24b04db91787e38a6842fe80a477b (patch) | |
| tree | 85812d968446d7690ccc2986108a4d26283daea6 | |
| parent | c230e600adeb35f4c174c68812712cf50a45fe44 (diff) | |
Updated.
| -rw-r--r-- | BUGS | 26 | ||||
| -rw-r--r-- | ccc/README | 4 | ||||
| -rw-r--r-- | coq/README | 4 | ||||
| -rw-r--r-- | etc/announce | 2 | ||||
| -rw-r--r-- | isa/README | 5 | ||||
| -rw-r--r-- | pgshell/README | 5 | ||||
| -rw-r--r-- | phox/README | 2 |
7 files changed, 17 insertions, 31 deletions
@@ -1,20 +1,5 @@ -*- outline -*- -* Bugs to be fixed before PG 3.5 is released; recently noted items - -The items below are known and will be fixed (or shifted to the list -below) before 3.5 is released. Please don't send email about these -(unless you can fix them). Please do send email about others. - -** Various menu problems with Emacs 21.2. - -PG menus may be added to wrong bar during autoload. See CHANGES for -temporary workaround. - - -================================================================= - - * Known Bugs and Workarounds for Proof General. Contact: mailto:da+pg-bugs@inf.ed.ac.uk @@ -54,11 +39,11 @@ An extra click on the toolbar may solve this. If you have problems, please customize `proof-toolbar-use-button-enablers' to nil to disable the enablers. -** Using C-g can leave script management in a mess. +** Using C-g can leave script management in a mess (rare). The code is not fully protected from Emacs interrupts. Workaround: Don't type C-g while script management is processing. -If you do, use proof-restart-scripting. +If you do, use proof-restart-scripting to be sure of synchronizing. ** Outline-mode does not work in processed proof script files @@ -89,7 +74,7 @@ to edit a file as it is being read by the proof assistant! -* Problems with particular Emacs versions +* Problems with particular Emacs versions [mostly historical] ** Buggy output fontification with Emacs 21.2 / X-Symbol 4.X @@ -124,8 +109,6 @@ adding this line to .emacs should help: (setq process-coding-system-alist '(("" . no-conversion))) - - ** XEmacs undo in the script buffer can edit the "uneditable region" Test case: Insert some nonsense text after the locked region. @@ -159,6 +142,3 @@ Several (odd) circumstances cause this version of Emacs to loop, in particular, when moving the cursor into multi-byte characters. Workarounds have been added to avoid this: you may see junk characters in the shell buffer as a side effect. - - - @@ -1,7 +1,9 @@ Proof General for the Casl Consistency Checker -Author: Christoph Lüth <cxl@informatik.uni-bremen.de> +Author: Christoph Lüth <cxl@informatik.uni-bremen.de> +================================================================= + This is a fairly straightforward instantiation of Proof General for the Casl Consistency Checker, CCC. @@ -6,10 +6,10 @@ Later contributions by Patrick Loiseleur, Pierre Courtieu, Status: supported Maintainer: Pierre Courtieu -Coq version: 6.3, 6.3.1, 7.x +Coq version: 6.3, 6.3.1, 7.x, 8.x Coq homepage: http://pauillac.inria.fr/coq/assis-eng.html -======================================== +=========================================================================== Coq Proof General has experimental multiple file handling for 6.3 versions. It does not have support for proof by pointing. diff --git a/etc/announce b/etc/announce index f563b096..a8d1aa31 100644 --- a/etc/announce +++ b/etc/announce @@ -29,7 +29,7 @@ Summary of changes since 3.4: . Keyboard hints and other messages displayed in minibuffer . Auxiliary modes bundled: X-Symbol and MMM Mode . Improved menus, user options, script colouring and active highlighting -. Many changes for compatibility with latest Emacsen and provers +. Many changes for compatibility with latest Emacsen (esp. GNU) and provers . Many other minor improvements and editing features . For Coq: a new "holes" system, for editing structured expressions . New instances of PG: Casl Consistency Checker, Shell Script @@ -3,12 +3,12 @@ Isabelle Proof General Written by David Aspinall, later with assistance from Markus Wenzel and David von Oheimb. -Status: supported +Status: supported Maintainer: David Aspinall Isabelle versions: Isabelle99-1, Isabelle99-2, Isabelle2002 Isabelle homepage: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ -======================================== +==================================================================== Isabelle Proof General has full support for multiple file scripting, with dependencies between theories communicated between Isabelle and @@ -25,6 +25,7 @@ were provided by Markus Wenzel. Check the value of isabelle-prog-name. + ======================================== $Id$ diff --git a/pgshell/README b/pgshell/README index ff6897e6..4dd96aa1 100644 --- a/pgshell/README +++ b/pgshell/README @@ -1,6 +1,9 @@ Proof General for shell scripts/simple command interpreters. -David Aspinall. +Author: David Aspinall +Status: Supported; experimental + +==================================================================== This instance of PG is handy just for using script management to cut-and-paste into a buffer running an ordinary shell of some kind. diff --git a/phox/README b/phox/README index c50f814f..4bbd01f1 100644 --- a/phox/README +++ b/phox/README @@ -7,7 +7,7 @@ Maintainer: Christophe Raffalli <Christophe.Raffalli@univ-savoie.fr> PhoX version: 0.8 PhoX homepage: http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html -======================================== +=========================================================================== This mode has support for script management with PhoX, and some other features ported from PhoX's own Emacs mode. |