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

2 files changed, 20 insertions, 1 deletions

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 *}