From cc6c3612ce5250aa3cd4453d67f34f0198484e0b Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 11 Dec 1998 17:13:08 +0000
Subject: Altered behaviour to allow retraction part-way through finished
 scripts. Previously Proof General was asked to unlock a file A.ML as soon as
 retraction in it happened.  Now Proof General is only asked to unlock the
 children of A.ML, although Isabelle records the fact that A.ML has been
 retracted.  (Which means that if A.ML is later re-linked, Proof General will
 correctly get told about it).

---
 isa/ProofGeneral.ML | 28 ++++++++++++++++++----------
 isa/isa.el          | 14 +++++++++++---
 2 files changed, 29 insertions(+), 13 deletions(-)

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index 23719994..293eac39 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -19,7 +19,7 @@ sig
 
    (* Processing used files *)
    
-   val retract_ML_file : string -> unit
+   val retract_ML_files_children : string -> unit
    val retract_thy_file : string -> unit
    val list_loaded_files : unit -> unit
    val restart : unit -> unit
@@ -27,6 +27,7 @@ sig
    val update : unit -> unit
    
    (* not used *)
+   val retract_ML_file : string -> unit
    val use_thy_and_update : string -> unit
 
    (*  visible only for testing *)
@@ -157,19 +158,20 @@ structure ProofGeneral : PROOFGENERAL =
     (* subroutine: retract a file and give message, if it hasn't
        been already reported to Proof General. *)
        
-    fun retract_file_and_give_message filename =
+    fun retract_file_and_give_message filename msg_flag =
       if filename="" orelse (filename mem !retracted_files) then ()
-      else (retract_msg filename;
+      else (if msg_flag then (retract_msg filename) else ();
 	    retracted_files := filename :: !retracted_files;
 	    ())
 
-    fun retract_file1 not_thy filename =
+    fun retract_file1 not_thy only_report_children filename =
      let val (path, tname) = split_filename filename
          fun show_msgs thy =
            let val (thy_file, ml_file) = get_thy_filenames (path_of thy) thy
             in (if not_thy then ()
-		   else retract_file_and_give_message thy_file; 
-		retract_file_and_give_message ml_file) end
+		   else retract_file_and_give_message thy_file true; 
+		retract_file_and_give_message ml_file 
+					(not only_report_children)) end
          (* Considered loaded if either theory or ML times set *)
 	 fun already_loaded thy =
            let val t = get_thyinfo thy
@@ -185,18 +187,24 @@ structure ProofGeneral : PROOFGENERAL =
       in      
        if already_loaded tname then
 	 (show_msgs tname; 
-	  map (retract_file1 false) (children_loaded tname); ())
+	  map (retract_file1 false false) (children_loaded tname); ())
        else ()
    end;
 
    (* retract a script file and all it's theory/script children,
-       but not it's parent theory. *)
+      but not it's parent theory. *)
+
+   val retract_ML_file = retract_file1 true false;
+
+   (* Same as above, but only give reports to Proof General for
+      the children.  *)
+
+   val retract_ML_files_children = retract_file1 true true;
 
-   val retract_ML_file = retract_file1 true;
 
    (* retract a theory file and all it's theory/script children *)
 
-   val retract_thy_file = retract_file1 false;
+   val retract_thy_file = retract_file1 false false;
 
 
    (* USING files.
diff --git a/isa/isa.el b/isa/isa.el
index 960d2730..c0118408 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -387,6 +387,12 @@ Resulting output from Isabelle will be parsed by Proof General."
   :type 'string
   :group 'isabelle-config)
 
+(defcustom isa-retract-ML-files-children-command "ProofGeneral.retract_ML_files_children \"%s\";"
+  "Sent to Isabelle to forget the descendants of an ML file.
+Resulting output from Isabelle will be parsed by Proof General."
+  :type 'string
+  :group 'isabelle-config)
+
 (defun isa-retract-thy-file (file)
   "Retract the theory file FILE. If interactive, use buffer-file-name."
   (interactive (list buffer-file-name))
@@ -501,15 +507,17 @@ Resulting output from Isabelle will be parsed by Proof General."
 (defun isa-find-and-forget (span)
   "Return a command to be used to forget SPAN."
   (save-excursion
+    ;; FIXME: bug here: too much gets retracted.
     ;; See if we are going to part way through a completely processed
     ;; buffer, in which case it should be removed from 
     ;; proof-included-files-list along with any other buffers
-    ;; depending on it.  NB: perhaps this is called too often for
-    ;; a bunch of spans in a region?
+    ;; depending on it.  However, even though we send the retraction
+    ;; command to Isabelle we don't want to *completely* unlock
+    ;; the current buffer.  How can this be avoided?
     (goto-char (point-max))
     (skip-chars-backward " \t\n") 
     (if (>= (proof-unprocessed-begin) (point))
-	(format isa-retract-ML-file-command 
+	(format isa-retract-ML-files-children-command
 		(file-name-sans-extension 
 		 (file-name-nondirectory
 		  (buffer-file-name))))
-- 
cgit v1.2.3