Add proof-cannot-reopen-processed-files to fix behaviour of multiple files for Isabelle.

6 files changed, 47 insertions, 2 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 2c80983b..917b0536 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1654,7 +1654,21 @@ setting to good effect.  If the proof assistant has more complex
 file dependencies then you should configure it to communicate with
 Proof General about the dependencies rather than using this setting."
   :type 'boolean
-  :group 'proof-shell)
+  :group 'proof-shell) ;; not really proof-shell
+
+(defcustom proof-cannot-reopen-processed-files nil
+  "Non-nil if the prover allows re-opening of already processed files.
+
+If the user has used Proof General to process a file incrementally,
+then PG will retain the spans recording undo history in the buffer
+corresponding to that file (provided it remains visited in Emacs).
+
+If the prover allows, it will be possible to undo to a position within
+this file.  If the prover does *not* allow this, this variable should
+be set non-nil, so that when a completed file is activated for 
+scripting (to do undo operations), the whole history is discarded."
+  :type 'boolean
+  :group 'proof-shell)  ;; not really proof shell
 
 ;; (defcustom  proof-shell-adjust-line-width-cmd nil
 
diff --git a/isa/BUGS b/isa/BUGS
index b874a599..41f992c3 100644
--- a/isa/BUGS
+++ b/isa/BUGS
@@ -4,6 +4,9 @@
 
 See also ../BUGS for generic bugs.
 
+See also ../isar/BUGS.  Isar is now main the instance for 
+Isabelle PG, the original Isabelle instance less supported.
+
 
 ** Issues with tracing mode 
 
diff --git a/isa/isa.el b/isa/isa.el
index 55405ac6..23da7ffe 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -229,6 +229,11 @@ and script mode."
    pg-subterm-help-cmd			"printyp (type_of (read \"%s\"))"
 
    ;; === MULTIPLE FILE HANDLING ===
+
+   ;; da: this next setting added for PG 3.5.  I think the theory
+   ;; loader changed at some point: originally this setting left as
+   ;; nil would have been okay.
+   proof-cannot-reopen-processed-files  t 
    proof-shell-process-file 
    (cons
     ;; Theory loader output and verbose update() output.
diff --git a/isa/todo b/isa/todo
index bd340089..4f077524 100644
--- a/isa/todo
+++ b/isa/todo
@@ -4,6 +4,10 @@
 
 See also ../todo for generic things to do, priority codes.
 
+See also ../isar/todo.  Isar is now main instance for PG, this
+instance less supported.
+
+
 ** D Isabelle: I think show_sorts -> show_types, how can we reflect this ?
 
 ** D Fix mode naming for Isabelle 
diff --git a/isar/isar.el b/isar/isar.el
index 1ea1f75e..bb7e48aa 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -274,6 +274,7 @@ See -k option for Isabelle interface script."
        'isabelle-convert-idmarkup-to-subterm 'pg-remove-specials)
    pg-subterm-help-cmd			"term %s" 
 
+   proof-cannot-reopen-processed-files  t
    proof-shell-process-file
    (cons
     ;; Theory loader output
@@ -443,7 +444,10 @@ proof-shell-retract-files-regexp."
        ;; open goal: skip and exit
        ((proof-string-match isar-goal-command-regexp str)
         (setq span nil))
-       ;; not undoable: fail and exit
+       ;; not undoable: fail and exit 
+       ;; [da: this is an odd case: it issues cannot_undo command to Isar,
+       ;;  which immediately generates an error, I think it's a bit confusing
+       ;; for the user]
        ((proof-string-match isar-undo-fail-regexp str)
         (setq answers nil)
         (setq ans (isar-cannot-undo str))
diff --git a/isar/todo b/isar/todo
index 15f9bcfe..f21dba72 100644
--- a/isar/todo
+++ b/isar/todo
@@ -4,6 +4,21 @@
 
 See also ../todo for generic things to do, priority codes.
 
+** C Improve handling of multiple files
+     We should recognize error messages from theory loader, in this form:
+
+	\<^sync>ProofGeneral.inform_file_processed "/home/da/projects/proofgen/cvs/ProofGeneral/etc/isar/multiple/A.thy"; \<^sync>; 
+### Unknown theory "A"
+### Theory loader: undefined theory entry for "A"
+### Failed to register theory "A"
+
+     (Although actually this case represents a bug elsewhere:
+      PG should not ask Isabelle to register some theory it doesn't know)
+     [Idea: maybe we need a sync-loaded-files possibility]
+
+     NB: Multiple file handling has been repaired compared with PG 3.4,
+     by adding the setting `proof-cannot-reopen-processed-files'.
+
 ** C Adjust imenu/fume to get sections/chapters usefully in tags
      Need to grab a prefix of text from the markup section {* Foo *}