retract_file also works on files without .thy partners.

1 files changed, 31 insertions, 28 deletions

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index fd2c322a..c6e683f8 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -169,10 +169,6 @@ end
 
 
 
-(* Some top-level commands for Proof General.
-   These could easily be customized to do different things.
-*)
-
 signature PROOFGENERAL =
 sig
    val kill_goal : unit -> unit
@@ -183,42 +179,49 @@ end
 
 structure ProofGeneral =
   struct
+    (* Some top-level commands for Proof General.
+       These easily could be customized to do different things.
+    *)
+
     fun kill_goal () = Goal "PROP no_goal_supplied";
     fun help () = print version;
     fun show_context () = the_context();
+
+    (*  Function used internally by Proof General to track
+        dependencies between theory and ML files. *)
+
     fun retract_file thy =
-    let fun file_msg x = if (x <> "") then
+     let fun file_msg x = if (x <> "") then
 			writeln ("Proof General, you can unlock the file "
 			     ^ (quote x))
 	               else ()
-      (* output messages for this theory *)
-    val (thy_file, ml_file) = get_thy_filenames (path_of thy) thy
-      val _ = file_msg thy_file
-      val _ = file_msg ml_file
-      (* now process this theory's children *)
-      val children = children_of thy;
-      val present = filter (is_some o get_thyinfo) children;
-      fun already_loaded thy =
-         let val t = get_thyinfo thy
-      in if is_none t then false
-         else let val {thy_time, ml_time, ...} = the t
-      in is_some thy_time andalso is_some ml_time end
-      end
-      val loaded = filter already_loaded present;
-   in      
-      if loaded <> [] then
-		(map retract_file loaded; ())
-      else ()
+         fun show_msgs thy =
+           let val (thy_file, ml_file) = get_thy_filenames (path_of thy) thy
+            in (file_msg thy_file; file_msg ml_file) end
+
+         fun already_loaded thy =
+           let val t = get_thyinfo thy
+           in if is_none t then false
+              else let val {thy_time, ml_time, ...} = the t
+           in is_some thy_time andalso is_some ml_time end
+         end
+
+         fun children_loaded thy = 
+         let val children = children_of thy
+	     val present = filter (is_some o get_thyinfo) children;
+          in filter already_loaded present end
+      in      
+       if already_loaded thy then
+	 (show_msgs thy; map retract_file (children_loaded thy); ())
+       else ()
    end;
   end;       
 
 
-(* duplicated code from thy_read.ML *)
-
-
-use "/home/da/isa-patches/thy_read.ML";
-open ThyRead;
+(* Turn on verbose update output, Proof General likes to parse it. *)
 update_verbose:=true;
+
+(* Let Proof General see the theories loaded in the logic image. *)
 update();