From 78b3a271a936bb12317287395250f552f87ce925 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 4 Sep 2001 16:35:34 +0000
Subject: Updates

---
 CHANGES | 18 ++++++++++++++++++
 INSTALL | 16 ++++++++++------
 2 files changed, 28 insertions(+), 6 deletions(-)

diff --git a/CHANGES b/CHANGES
index 3925765a..6ed6fa64 100644
--- a/CHANGES
+++ b/CHANGES
@@ -38,6 +38,21 @@
      Also, for XEmacs, there are now (trivial) help messages in echo
      area describing the highlighted region under the mouse.
 
+*** Experimental features and new user option
+
+     There's a new user option `proof-experimental-features' which
+     is nil by default.  If you set it to t, you will (maybe after
+     restarting Proof General) enable certain experimental features.
+ 
+     In this release, the experimental features are: 
+
+        Context menu options to move spans up/down
+        Context menu dependency commands (Isabelle only, see below)
+
+     To customize this from the menu:
+  
+        Proof General -> Customize -> User Options -> Experimental features
+
 *** Proof General startup script welcomes user
  
      The "binary" (startup script) bin/proofgeneral now loads
@@ -126,6 +141,9 @@
    restart.  (This behaviour will improve once better integrated 
    with Isabelle).
 
+   NB this is classed as an experimental feature, so you must set
+   proof-experimental-features to enable it.
+   
    Not yet documented.    Comments and suggestions welcome.
 
 
diff --git a/INSTALL b/INSTALL
index e26ed497..7f7f50f6 100644
--- a/INSTALL
+++ b/INSTALL
@@ -105,12 +105,16 @@ Byte Compilation.
 -----------------
 
 Compilation of the Emacs lisp files improves efficiency but can
-sometimes cause compatibility problems.  It is not supported in this
-release.  If you want to experiment nonetheless, you can compile Proof
-General by typing 'make' in the directory where you installed it.
-This will result in lots of warnings and error messages most of which
-can be ignored. Check the Makefile sets EMACS to your Emacs
-executable.
+sometimes cause compatibility problems.  It is not properly supported
+in this release, because testing for these compatibility problems
+takes too much time.  If you want to experiment nonetheless, you can
+compile Proof General by typing 'make' in the directory where you
+installed it.  This will result in lots of warnings and error messages
+most of which can be ignored. Some files cannot be properly
+byte-compiled at the moment because they contain settings which depend
+on run-time; these will be deleted by the Makefile.  Use 'make clean'
+to remove all .elc files in case of problems.  Check the Makefile sets
+EMACS to your Emacs executable.
 
 
 Site-wide Installation
-- 
cgit v1.2.3