New/updated information files

3 files changed, 62 insertions, 15 deletions

diff --git a/isa/BUGS b/isa/BUGS
new file mode 100644
index 00000000..0ec5719a
--- /dev/null
+++ b/isa/BUGS
@@ -0,0 +1,33 @@
+-*- mode:outline -*-
+
+* Isabelle Proof General Bugs
+
+See also ../BUGS for generic bugs.
+
+
+** "Stack overflow in regexp".  
+
+This problem is caused by a poor regexp and large proofstates.  It
+needs some small alterations to other proof assistant regexps, so will
+be fixed in 3.2.  In the meantime, a workaround is to reduce the
+number of subgoals displayed.
+
+** set proof_timing is problematic
+
+It will make the goals display disappear during proof.  This is
+because Proof General only displays goals output that appears *after*
+Isabelle messages, but Isabelle prints the timing message after the
+goals are displayed.
+
+** General difficulty with proof scripts containing ML structures, etc.  
+
+Proof General does not understand full ML syntax(!), so it will be
+confused by structures which contain semi-colons after declarations,
+for example.  Also, it cannot undo function declarations.  See the
+section on ML files in the manual for more details.
+
+** Blocking when processing multiple files, beginning from a .ML file.
+
+Proof General will block the Emacs process when it is waiting for a
+theory file (and it's ancestors) to be read as scripting is turned on.
+To avoid this, assert the theory file rather than the ML file.
diff --git a/isa/README b/isa/README
index 766cc256..83e13d13 100644
--- a/isa/README
+++ b/isa/README
@@ -5,10 +5,25 @@ Markus Wenzel and David von Oheimb.
 
 $Id$
 
+Status:		   supported
+Maintainer:	   David Aspinall
+Isabelle version:  99
+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
 Proof General.  It has a mode for editing theory files taken from
 Isamode.
 
-There is no support for proof by pointing yet.
+There is proper support for X Symbol, using the Isabelle print mode
+for X Symbol tokens.  Many Isabelle theories have X Symbol syntax
+already defined and it's easy to add to your own theories.
+
+There is no support for proof by pointing yet, and no tags program.
+
+The script `interface' and file 'interface-setup.el' are used to start
+Isabelle Proof General via the 'Isabelle' shell command.  These files
+were provided by Markus Wenzel.
 
diff --git a/isa/todo b/isa/todo
index da20d04a..eaad888b 100644
--- a/isa/todo
+++ b/isa/todo
@@ -1,15 +1,14 @@
 -*- mode:outline -*-
 
-* See also ../todo for generic things to do, priority codes.
-
 * Things to do for Isabelle
-===========================
 
-C Investigate fix for looping rewriting in Isabelle.  Continual
+See also ../todo for generic things to do, priority codes.
+
+** C Investigate fix for looping rewriting in Isabelle.  Continual
   and frequent messages from the prover lock out the user.
   Is there any easy way of fixing this?
   
-C X-Symbol support for theory files: bugs at the moment, because
+** C X-Symbol support for theory files: bugs at the moment, because
   of duplicate calls to proof-x-symbol-mode and mess with
   font-lock initialization.  Problem with current version:
   visit a.thy, b.thy then turn on xsym.  Broken in b.thy.
@@ -19,22 +18,22 @@ C X-Symbol support for theory files: bugs at the moment, because
   [DvO reports okay].
   (May need to split extra modes into two parts?)
 
-B auto-adjust Pretty.setmargin when window is resized.  Use
+** B auto-adjust Pretty.setmargin when window is resized.  Use
   generic code once it's implemented.
 
-D Implement completion for Isabelle using tables generated by
+** D Implement completion for Isabelle using tables generated by
   the running process.  Ideally context sensitive.
   Would be a nice addition. (1 week)
 
-D Add useful specific commands for Isabelle.  Many could
+** D Add useful specific commands for Isabelle.  Many could
   be added.  Would be better to merge in Isamode's menus.
   (however, probably 2 week's work to bring together Isamode 
    and proof.el, making some of Isamode generic)
 
-D Switching to other file with C-c C-o could be more savy
+** D Switching to other file with C-c C-o could be more savy
   with file names and extensions (use some standard function?)
 
-X weird bug: interrupting Isabelle process (under sml-nj) sometimes
+** X weird bug: interrupting Isabelle process (under sml-nj) sometimes
   doesn't return, why? (see first half of interrupt error only:
 
     *** Interrupt.
@@ -58,15 +57,15 @@ X weird bug: interrupting Isabelle process (under sml-nj) sometimes
     ProofGeneral.isa_restart(); 
     /usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2af9e01b
 
-X Add ability to choose logic.  Maybe not necessary: can use default
+** X Add ability to choose logic.  Maybe not necessary: can use default
   set in Isabelle settings nowadays, in the premise that most people
   stick to a particular logic?   But then no support for loading
   user-saved databases.  (ponder this)
 
-X Write perl scripts to generate TAGS file for ML and thy files.
-  (6h, I've completely forgotten perl).  
+** X Write perl scripts to generate TAGS file for ML and thy files.
+  (6h, any volunteers?).  
 
-X Manage multiple proofs, perhaps by automatically inserting
+** X Manage multiple proofs, perhaps by automatically inserting
   push_proof() and pop_proof() commands into the proof script.
   But would lead to unholy mess for script management!