Updates

7 files changed, 177 insertions, 51 deletions

diff --git a/etc/announce b/etc/announce
index 382aca11..fd2b6d2c 100644
--- a/etc/announce
+++ b/etc/announce
@@ -1,4 +1,3 @@
-Reply-To: "Proof General Maintainer <proofgen@dcs.ed.ac.uk>"
 To: coq-club@pauillac.inria.fr,
     isabelle-users@cl.cam.ac.uk,
     lego-club@dcs.ed.ac.uk,
@@ -33,54 +32,58 @@ Subject: Proof General --- Version 3.0 release
 
    A Generic Emacs interface for Interactive Proof Assistants
 
-            http://zermelo.dcs.ed.ac.uk/home/proofgen
+           http://zermelo.dcs.ed.ac.uk/home/proofgen
+
+           contact: David Aspinall <da@dcs.ed.ac.uk>
 
 		 =========================
 
-Proof General is supplied ready-customised for LEGO, Coq, and
-Isabelle.  It includes these features (amongst others):
-
- . Script management: files and regions of files processed by
-   prover have a blue background and are read-only; the state
-   of the proof assistant is reflected inside the editor.
-   Script management works across multiple files for
-   LEGO and Isabelle.
-   
- . A toolbar for building and replaying proofs and interacting
-   with the proof assistant.
- 
- . Syntax highlighting of proof scripts and prover output
- 
- . Simplified communication: the proof assistant is run in
-   an Emacs shell buffer, but by default it is hidden from view
-   and only the most recent messages and proofstate are displayed
-   to the user, simplifying the dialogue.
-   
- . Menu for jumping to theorems in a proof script, Emacs outlining
-   of proof scripts
-   
- . Provision to easily run proof assistant on a remote host
-
-Script management is the main feature.  
+Proof General is an Emacs interface for developing proof scripts.
+It can be instantiated for the proof assistant of your choice,
+and is supplied ready-customised for Isabelle, Coq, and LEGO.
+
+Proof General includes these features, amongst others:
+
+. Script management: proof assistant state reflected in editor
+. Toolbar and menus: commands for building and replaying proofs
+. Syntax highlighting of proof scripts and prover output
+. Integration with X-Symbol to provide logical symbols, etc
+. Simplified communication: proof assistant verbosity hidden
+. Menu for jumping to theorems in a proof script
+. Provision to easily run proof assistant on a remote host
 
 Summary of changes since 2.1:
 
- . Six new toolbar buttons, enabled depending on context
- . Reorganized and improved menus 
- . New function to search for theorems 
- . Lots more fine-grained improvements, for full details
-   http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneral/CHANGES
+. Six new toolbar buttons, enabled depending on context
+. Improved and reorganized menus and keybindings, options settings
+. Easier to adapt to new systems, comes with example (30 setqs)
+. New function to search for theorems 
+. Lots more fine-grained improvements, for full details
+  http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneral/CHANGES
 
 The user manual contains full details, and is available on-line at: 
 http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneral/doc/ProofGeneral_toc.html
 
+Proof General needs a recent version of Emacs to run with, and it much
+prefers XEmacs to FSF GNU Emacs.  Proof General 3.0 has been tested
+with XEmacs 21.1 and Emacs 20.4.  (It should work back to XEmacs 20.4
+and Emacs 20.2, though).  
+
+Installing Proof General is easy.  Give it a try!
+
+ - David Aspinall <da@dcs.ed.ac.uk>
+
+
+
 The rest of this announcement contains notes addressed to different
 user communities: LEGO, Coq, and Isabelle; users of other proof
 assistants, user-interface/theorem-proving researchers and, finally,
 Emacs gurus.
 
+
 To users of LEGO, Coq, and Isabelle:
 ------------------------------------
+
 Proof General 3.0 has several new features as well as bug fixes and
 improvements over versions 2.1 and 2.0.  It supports the latest
 theorem prover versions: LEGO 1.3.1, Coq 6.3 and Isabelle 99.
@@ -88,11 +91,7 @@ theorem prover versions: LEGO 1.3.1, Coq 6.3 and Isabelle 99.
 Please try it and let us know what you think of it!
 
 We have worked hard on the user documentation, and on making Proof
-General robust and easy to install. Ideally you should use it with
-XEmacs, but it also works with limited features in FSF GNU Emacs. 
-
-We have tested on XEmacs 21.1 and Emacs 20.2, 20.3. (It probably works
-with earlier versions of either Emacs but we cannot guarantee this).
+General robust and easy to install.
 
 
 To users of other proof assistants:
@@ -110,7 +109,7 @@ General for it, and let us know how you get on.
 To user-interface/theorem-proving researchers:
 ---------------------------------------------- 
 Proof General provides a unified interface to different theorem
-provers. The advantage is that a novice who understands the Proof
+provers.  The advantage is that a novice who understands the Proof
 General interface can inspect and replay proofs in any of the theorem
 provers supported, without knowing the specific commands needed to
 drive them.  Moreover, by implementing your user-interface ideas in
@@ -120,20 +119,22 @@ large community of both novice and expert proof assistant users.
 A desirable avenue towards further and easier unification would be to
 invent a unified proof script (input) language and proof-state
 (output) language for theorem provers. The Proof General experience
-could provide useful insight into such a project. We'd be interested
-to hear from workers interested in collaborating in this area.
+could provide useful insight into such a project.  I'd be keen to hear
+from workers interested in collaborating in this area.
+
 
-To Emacs gurus:
----------------
-If you are an Emacs guru and want to contribute to the development of
-Proof General, please join in!  There are plenty of exciting avenues
-for improving this tool, for example, to add proof by pointing
-facilities (a basis already exists for LEGO), and a theory browser.
+To Emacs gurus: 
+--------------- 
+If case happen to be an Emacs guru also interested in interactive
+proof, we want you to contribute to the development of Proof General!
+Please join in!  There are plenty of exciting avenues for improving
+this tool, for example, to add proof by pointing facilities (a basis
+already exists for LEGO), and a theory browser.
 
 Apart from proof assistants, script management makes sense for many
 other systems or languages with an interactive shell-like interpreter.
-We would be interested to hear from any Emacs developers interesting
-in adapting Proof General's script management for development in Lisp,
+I would be keen to hear from any Emacs developers interesting in
+adapting Proof General's script management for development in Lisp,
 SML, or other languages.
 
 
diff --git a/etc/junk.el b/etc/junk.el
index 3f66f664..dadf1bb6 100644
--- a/etc/junk.el
+++ b/etc/junk.el
@@ -83,3 +83,58 @@ arrive."
 
 
 
+;; was is proof-shell, never used.
+(defun proof-shell-strip-eager-annotation-specials (string)
+  "Strip special eager annotations from STRING, returning cleaned up string.
+The input STRING should be annotated with expressions matching
+proof-shell-eager-annotation-start and eager-annotation-end.
+We only strip specials from the annotations."
+  (let* ((mstart (progn
+		   (string-match proof-shell-eager-annotation-start string)
+		   (match-end 0)))
+	 (mend	 (string-match proof-shell-eager-annotation-end string))
+	 (msg	 (substring string mstart mend))
+	 (strtan (substring string 0 mstart))
+	 (endan	 (substring string mend)))
+    (concat
+     (proof-shell-strip-special-annotations strtan)
+     msg
+     (proof-shell-strip-special-annotations endan))))
+     
+
+
+;; 2. proof-find-and-forget-fn
+;;
+;; This calculates undo operations outwith a proof.  If we retract
+;; before a "Goal" command, proof-kill-goal-command is sent, followed
+;; by whatever is calculated by this function.
+;;
+;; Isabelle has no concept of a linear context, and you can happily
+;; redeclare values in ML.  So forgetting back to the declaration of a
+;; particular something makes no real sense.  
+;; The function is given a trivial implementation in this case.
+;;
+;; Find LEGO or Coq's implementation of this function to see how to
+;; write it for proof assistants that can do this.
+
+
+
+;; FIXME: this is supposed to be a handy way of swapping
+;; between goals and response buffer.  Never mind.
+;(defun proof-bury-buffer-after (buf)
+;  (if (and (string-match "XEmacs" emacs-version) ; XEmacs speciality
+;	   (buffer-live-p buf))
+;      (bury-buffer (current-buffer) buf)
+;    (bury-buffer)))
+
+;(defun proof-bury-buffer-after-goals ()
+;  (interactive)
+;  (proof-bury-buffer-after proof-goals-buffer))
+
+
+
+;(defun proof-bury-buffer-after-response ()
+;  (interactive)
+;  (if proof-response-buffer
+;      (with-current-buffer proof-response-buffer
+;	(proof-bury-buffer-after proof-goals-buffer))))
diff --git a/etc/mailinglist-bait b/etc/mailinglist-bait
new file mode 100644
index 00000000..395e67d4
--- /dev/null
+++ b/etc/mailinglist-bait
@@ -0,0 +1,34 @@
+Dear Proof General users,
+
+This is a newsy note to tell you that Proof General 3.0 is ready for
+release Very Soon Now.  In the meantime, I'd be very grateful to
+anyone who can test a pre-release and tell me how it goes.  (I try to
+do as much testing as I can, but it's getting more difficult as more
+proof assistants are supported).
+
+I'm quite excited about this release.  I've concentrated on usability,
+making the code clean and robust, and making PG easier to adapt for
+new proof assistants.  But there are some important new features too...
+
+David von Oheimb's patches for X-Symbol have been made generic now,
+and easy to turn on and off.  I've added some basic support for Coq
+and LEGO, so Greek letters and symbols like /\ and -> display as you
+would like.  Break free from ASCII!
+
+Proof-by-pointing has been resurrected!  The interface relies on the
+proof assistant to construct the proof commands, and the only prover
+supported currently LEGO.  One reason PBP was disabled was that LEGO's
+implementation is experimental and incomplete.  But I hope that people
+can see PBP almost working in LEGO and be encouraged to implement it
+for other provers.  We can certainly hope for support in Coq, since
+the CtCoq proof-by-pointing code has been moved into the Coq kernel
+now.  I hope the Coq community can encourage somebody to do this.
+
+Visit http://zermelo.dcs.ed.ac.uk/~proofgen/ for more.
+
+Best regards,
+
+ - David.
+
+
+
diff --git a/etc/testing-log.txt b/etc/testing-log.txt
index 5dce8d54..08528479 100644
--- a/etc/testing-log.txt
+++ b/etc/testing-log.txt
@@ -1,3 +1,15 @@
+Tue Nov 16 15:28:51 GMT 1999
+
+ Tested automatic multiple file handling: see etc/demoisa
+
+ Tested FSF Emacs, after fixing several things.
+
+ Tested proof by pointing in LEGO.  Fixes for bugs,
+ empty pbp response, and added a useful click
+ (C-button 3) for undoing and deleting the last 
+ pbp command.  Can now prove example.l by PBP.
+ Proof-by-pointing lives!
+
 Thu Nov 11 19:05:39 GMT 1999
 
  Tested response buffer display: see isa/message-test.ML
diff --git a/html/download.phtml b/html/download.phtml
index 4eceec96..a0648543 100644
--- a/html/download.phtml
+++ b/html/download.phtml
@@ -41,7 +41,7 @@ you may wish to check the
 This version of Proof General has been tested
 with XEmacs 20.4, XEmacs 21 and FSF Emacs 20.3.<br>
 It supports Coq version 6.3, LEGO version 1.3.1 and
-Isabelle version 99.
+some pre-release versions of Isabelle version 99.
 <p>
 Check the <?php fileshow("ProofGeneral-2.1/CHANGES","CHANGES"); ?> file
 for a summary of changes since version 2.0.
@@ -215,6 +215,27 @@ we can make our CVS repository accessible to you.  Please
 Please note that we do not support these old releases in any way.
 </p>
 
+
+<h4>Proof General Version 2.1, released 24th August 1999</h4>
+
+<p>
+This version of Proof General has been tested
+with XEmacs 20.4, XEmacs 21 and FSF Emacs 20.3.<br>
+It supports Coq version 6.3, LEGO version 1.3.1 and
+some pre-release versions of Isabelle version 99.
+<ul>
+  <li> gzip'ed tar file: 
+      <?php download_link("ProofGeneral-2.1.tar.gz") ?>
+  </li>
+ <li> Linux RPM package:
+      <?php download_link("ProofGeneral-2.1-1.noarch.rpm") ?>
+     <br>
+     The source RPM is 
+      <?php download_link("ProofGeneral-2.1-1.noarch.rpm","here") ?>.
+ </li>
+</ul>
+
+
 <h4>Proof General Version 2.0, released 16th December 1998</h4>
 
 <p>
diff --git a/html/functions.php3 b/html/functions.php3
index efa23165..39166af4 100644
--- a/html/functions.php3
+++ b/html/functions.php3
@@ -58,7 +58,7 @@ function dt($string) {
 /* FIXME: for now, just inline them. */
 
 function footnote ($text) {
-   print "<p><small><i>[" . $text . "]</i></small></p>";
+   print "<p><i><small>[" . $text . "]</small></i></p>";
 }
 
 /* A hyper-link with optional mouse over text.
diff --git a/html/main.phtml b/html/main.phtml
index 548edc72..21409081 100644
--- a/html/main.phtml
+++ b/html/main.phtml
@@ -48,7 +48,7 @@ including:
          <a href="http://www.dcs.ed.ac.uk/~hhg">Healfdene Goguen</a>. 
          <br>
 	  Maintained by 
-	    <a href="mailto:courtieu@lri.fr">Pierre Courtieu &lt;courtieu@lri.fr&gt;</a>.
+	    <a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>.
         </div>
     </td>
  </tr>
@@ -103,6 +103,9 @@ made available in our developers release.
 </p>
 
 <p>
+To read more about what features Proof General
+provides, <a href="features.phtml">click here</a>.
+<br>
 To see what Proof General looks like in use, have a look at this
 <a href="screenshot.phtml">screenshot</a>.
 </p>