Improvements for multiple files and robustness: keep a copy of

the initial theory database state, and add a restart command.

2 files changed, 23 insertions, 4 deletions

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index b0bc0c0b..1663953d 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -37,6 +37,7 @@ sig
    val retract_thy_file : string -> unit
    val list_loaded_files : unit -> unit
    val update : unit -> unit
+   val restart : unit -> unit
    
    (*  visible only for testing *)
    val loaded_parents_of : string -> string list
@@ -44,6 +45,7 @@ sig
    val apply_and_update_files : ('a -> 'b) -> 'a -> unit
    val use_thy_and_update : string -> unit  (* not used *)
    val use_thy : string -> unit
+   val initial_loaded_thys : thy_info Symtab.table ref
    val special_theories : string list ref
    val retracted_files : string list ref
 end;
@@ -69,6 +71,9 @@ structure ProofGeneral : PROOFGENERAL =
     (* Cache of retracted files: see notes below. *)
     val retracted_files = ref [] : string list ref;
 
+    (* Copy of theory database *)
+    val initial_loaded_thys = ref (!loaded_thys);
+
     (* Messages to Proof General *)
 
     fun retract_msg x = writeln ("Proof General, you can unlock the file "
@@ -116,7 +121,6 @@ structure ProofGeneral : PROOFGENERAL =
    *)
    fun list_loaded_files () =
    let
-     val thys_list = Symtab.dest (!loaded_thys)
      val _ = retracted_files := []
    in     
     (writeln "Setting loaded files list...";
@@ -124,6 +128,18 @@ structure ProofGeneral : PROOFGENERAL =
      writeln "Done.")
    end
 
+   (* RESTARTING *)
+
+   fun restart () =
+     let val _ = (loaded_thys := !initial_loaded_thys)
+         val _ = (retracted_files := [])
+      in
+         (list_loaded_files();
+          clear_response_buffer();
+          writeln "Isabelle Proof General: Isabelle process ready!")
+      end;
+
+
     (*
       RETRACTION:
          We keep some state here to record what files Proof General
@@ -244,6 +260,7 @@ structure ProofGeneral : PROOFGENERAL =
     (* Use a theory file but not it's top-level ML file *)
     val use_thy = use_thy1 use_thy_no_topml;
 
+    
 
    (* Function to do an "update" operation.
        This is like the use operation above except that we
@@ -386,9 +403,7 @@ print_current_goals_fn := print_current_goals_with_plain_output;
 
 (* Get Proof General to cache the loaded files.  *)
 
-ProofGeneral.list_loaded_files();
-ProofGeneral.clear_response_buffer();
-writeln "Isabelle Proof General: Isabelle process ready!";
+ProofGeneral.restart();
 
 
 
diff --git a/isa/isa.el b/isa/isa.el
index 1bdfc55b..8a5421d1 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -180,6 +180,9 @@ no regular or easily discernable structure."
    ;; initial command configures Isabelle by hacking print functions.
    proof-shell-init-cmd
      (concat "use \"" proof-home-directory "isa/ProofGeneral.ML\";")
+   proof-shell-restart-cmd		"ProofGeneral.restart();"
+   proof-shell-quit-cmd			"exit 1;"
+   
    proof-shell-eager-annotation-start   "\360\\|\362\\|\364"
    proof-shell-eager-annotation-end     "\361\\|\363\\|\365"
 
@@ -346,6 +349,7 @@ isa-proofscript-mode."
 (define-key map "\C-c\C-b" 'isa-process-thy-file)
 (define-key map "\C-c\C-u" 'isa-retract-thy-file)))
 
+;; FIXME: could test that the buffer isn't already locked.
 (defun isa-process-thy-file (file)
   "Process the theory file FILE.  If interactive, use buffer-file-name."
   (interactive (list buffer-file-name))