Updated

4 files changed, 43 insertions, 23 deletions

diff --git a/CHANGES b/CHANGES
index 47f5f1ed..552c3dd8 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,8 +7,9 @@
 
 *** HOL 98 (http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html)
 
-   by David Aspinall.  This is a bare-bones Proof General instance
-   only, hopefully to entice HOL users so that someone may improve it.
+   by David Aspinall.  This is a fairly basic Proof General instance
+   only, hopefully to entice HOL users so that one of them may improve it.
+   I don't plan to maintain or improve this instantiation myself.
    See README in the hol98 directory for more details.
 
 *** Plastic (http://www.dur.ac.uk/CARG/plastic.html)
@@ -20,6 +21,12 @@
 
 ** Generic Changes
 
+*** Names of shell, goals, script buffers now based on proof assistant name
+
+  Basing the name on the command isn't very abstract and leads to strange 
+  names for some provers, "coqtop" and "hol.unquote".  Now we just use
+  the lower case of the proof assistant name.
+
 *** README file added for each supported prover, explaining support.
 
 *** Fixes for supporting Japanese versions of Emacs which have older CL macs.
@@ -50,7 +57,7 @@
   appear.  
   
   The default setting for proof-shell-process-connection-type is made
-  by examining the ARCH environment variable.  If this contains "sun"
+  by calling uname, if possible.  If this contains "sun"
   then proof-shell-process-connection-type is set to nil for using
   pipes.  Otherwise we use ptys which are to be prefered over pipes
   because pipes can become full or lose data, and pipes don't work
@@ -60,7 +67,12 @@
   
 *** Added new configuration hook:  proof-shell-pre-interrupt-hook
 
-  This is 
+  This is added particularly for Isabelle running with Poly/ML,
+  which requires interaction after an interrupt.
+
+*** Minor cosmetic improvements
+
+  Name of proof assistant "Start Isabelle" etc. in menu.
 
 ** Coq Changes
 
@@ -72,7 +84,7 @@
 
 ** Isabelle Changes
 
-***
+*** Fix for Poly/ML with interrupts: use proof-shell-pre-interrupt-hook
 
 
 ** Isar Changes
diff --git a/hol98/README b/hol98/README
index 38cbfe26..84e4cc5a 100644
--- a/hol98/README
+++ b/hol98/README
@@ -6,18 +6,18 @@ $Id$
 
 This is a "technology demonstration" of Proof General for HOL 98.
 
-It may well work with other versions of HOL, but is untested (please
-let me know if you try).
+It may work with other versions of HOL, but is untested (please let me
+know if you try).
 
 It has basic script management support, with a little bit of
 decoration of scripts and output.
 
-There is support for x-symbols, but not using a proper token language.
-Try writing "philosophy" !
+There is support for x-symbols, but not using a proper token
+language.  Try writing "philosophy" !
 
 I have written this in the hope that somebody from the HOL community
-will adopt it and turn it into a proper instantiation of 
-Proof General.
+will adopt it, maintain and improve it, and thus turn it into a proper
+instantiation of Proof General.
 
 ------------------
 
@@ -25,12 +25,12 @@ Note:
 
 There are some problems at the moment.  HOL proof scripts often use
 batch-oriented single step tactic proofs, but Proof General does not
-offer an easy way to edit these kind of proofs.  The "Boomburg" Emacs
-interface by Koichi Takahashi and Masima Hagiya addressed this, and to
-some extent so does the Emacs interface supplied with HOL.  Perhaps
-one of these could be embedded inside Proof General.  Implemented in
-a generic way, managing batch vs interactive proofs would also be
-useful for Isabelle.
+offer an easy way to edit these kind of proofs.  The "Boomburg-HOL"
+Emacs interface by Koichi Takahashi and Masima Hagiya addressed this,
+and to some extent so perhaps does the Emacs interface supplied with
+HOL.  Perhaps one of these could be embedded/reimplemented inside
+Proof General.  Implemented in a generic way, managing batch vs
+interactive proofs would also be useful for Isabelle.
 
 Another problem is that HOL scripts sometimes use SML structures,
 which can cause confusion because Proof General does not really parse
diff --git a/hol98/example.sml b/hol98/example.sml
index 04b3b062..64858140 100644
--- a/hol98/example.sml
+++ b/hol98/example.sml
@@ -7,6 +7,7 @@
 g `A /\ B ==> B /\ A`;
 e DISCH_TAC;
 e CONJ_TAC;
+ 
 
 
 (* Ooops, I'm stuck now.  Can somebody help?? 
diff --git a/todo b/todo
index 43c6219d..5028fc37 100644
--- a/todo
+++ b/todo
@@ -45,8 +45,19 @@ X (Low)		e.g. probably not worth spending time on
 * Scheduled improvements for 3.2
 ================================
 
-** Scheme to detect type of buffer
-** More proof assistants supported
+B Scheme to detect type of buffer and choose between possible modes.
+  Help select Isar over Isa, maybe sml over HOL etc?
+
+B Yet more proof assistants supported.  Perhaps we will introduce
+  class of "unsupported" Proof General interfaces.
+
+B Add to proof-config those variables created in proof-easy-config for
+  font lock and syntax entries.  Use these instead of primitive
+  elisp in the other configs, too.
+
+C More flexible help configuration is needed.  HOL has some nice
+  on-line help but no way in PG to help by library.  Perhaps
+  a help browser is needed?  At least, optional arg to help command.
 
 
 
@@ -55,10 +66,6 @@ X (Low)		e.g. probably not worth spending time on
 * Things to in the generic interface
 ====================================
 
-C More flexible help configuration is needed.  HOL has some nice
-  on-line help but no way in PG to help by library.  Perhaps
-  a help browser is needed?
-
 B Manual improvements before techreport publishing (see notes at end also):
   - Mention configuring function menus, outline.
   - Consider splitting up chapter 9?