Updated.

4 files changed, 34 insertions, 6 deletions

diff --git a/BUGS b/BUGS
index be1ae67d..83a26034 100644
--- a/BUGS
+++ b/BUGS
@@ -22,6 +22,8 @@ typing:
 
   $  LANG=en_GB xemacs &
 
+Another solution is to set LANG inside a file ~/.i18n, which will
+be read the shell.  This will affect all applications, though.
 [ suggestions for a better workaround inside Emacs would be welcome ]
 
 
diff --git a/CHANGES b/CHANGES
index efa3eba6..2148159d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,11 @@
 
 ** Generic changes
 
+*** Options and proof assistant settings improvements
+
+Facility to reset to default values added, and saving
+of (just) proof assistant settings.
+
 *** Display management: added shrink-windows-tofit option
 
 Attempt to shrink output windows to fit their contents in
@@ -25,9 +30,24 @@ case it is less than 1/2 the window height.  In progress.
 Please report any problems/annoyances which may be unexpected.
 NB: Not yet enabled for Isabelle/Isar.
 
-
 *** Tweaks to menus,  colours
 
 Electric terminator menu option more visible. 
 Reduce contrast for mouse highlighting of regions.
 
+*** Support formatted input which contains newlines [for Coq]
+
+A patch from Stefan Monnier, to allow Coq input to have newlines
+remaining, so that input formatting is not broken.  A much better way
+to address this would be to alter the Coq output routines so that they
+do not print multiple identical prompts for continued lines.  
+[this is in testing: please notify me of problems in other provers]
+
+
+** Changes for Isabelle
+
+Beginnings of support PGIP protocol (work in progress with Isabelle
+CVS version).  Presently allows Isabelle to configure Proof General.
+
+CURRENTLY SUPPORT FOR CURRENTLY RELEASED ISABELLE VERSIONS IS BROKEN
+
diff --git a/Makefile b/Makefile
index 0f1e8f30..2aac5500 100644
--- a/Makefile
+++ b/Makefile
@@ -33,11 +33,10 @@ BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (con
 EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done)
 ELC=$(EL:.el=.elc)
 
-# These files may work now, but BC is not yet guaranteed in 3.4.
-# [currently broken for prover instances]
-# proof-toolbar.elc proof-menu.elc proof-indent.elc proof-x-symbol.elc
-BROKENELC=proof-menu.elc # easy-menu-define expanded too early.
-# NB: calls to proof-defshortcut also broken, evaluates define-key.
+# Some parts of code were not compile safe, because of macros
+# being expanded too early (e.g. proof-defshortcut, easy-menu-define)
+# This should be fixed for 3.5, although careful testing is required.
+BROKENELC=
 
 .SUFFIXES:	.el .elc
 
diff --git a/todo b/todo
index 747003e6..7d7d80a8 100644
--- a/todo
+++ b/todo
@@ -32,6 +32,13 @@ X (Low)		e.g. probably not worth spending time on
 
 ** 2. Things to do in the generic interface
 
+*** A settings configuration for Isabelle: add backwards
+    compatibility for older versions of Isabelle.  
+    Waiting for Isabelle to provide some easy version
+    checking.
+
+*** B Cleanup display during settings processing.
+
 *** A fix display anomaly for Isar output with shrink windows:
     display splits window unexpectedly.