Added clear-goals-buffer stuff, asked for response to be left after use_thy.

2 files changed, 33 insertions, 17 deletions

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index f3ef5174..23719994 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -15,6 +15,7 @@ sig
    val show_context : unit -> theory
    val repeat_undo : int -> unit
    val clear_response_buffer : unit -> unit
+   val clear_goals_buffer : unit -> unit
 
    (* Processing used files *)
    
@@ -39,17 +40,6 @@ end;
 
 structure ProofGeneral : PROOFGENERAL =
   struct
-    (* Some top-level commands for Proof General. *)
-
-    fun kill_goal () = (Goal "PROP no_goal_supplied"; ())
-    fun help () = print version;
-    fun show_context () = the_context();
-
-    (* Function used by undo operation *)
-    
-    fun repeat_undo 0 = ()
-      | repeat_undo n = (undo(); repeat_undo (n-1));
-
     (* State *)
 
     (* Theories which have no .thy or .ML files *)	
@@ -71,6 +61,23 @@ structure ProofGeneral : PROOFGENERAL =
 
     fun clear_response_buffer () =
        writeln("Proof General, please clear the response buffer.");
+
+    fun clear_goals_buffer () =
+       writeln("Proof General, please clear the goals buffer.");
+
+
+    (* Some top-level commands for Proof General. *)
+
+    fun kill_goal () = (Goal "PROP no_goal_supplied"; clear_goals_buffer())
+    fun help () = print version;
+    fun show_context () = the_context();
+
+    (* Function used by undo operation *)
+    
+    fun repeat_undo 0 = ()
+      | repeat_undo n = (undo(); repeat_undo (n-1));
+
+
        
 
     (*
@@ -128,10 +135,12 @@ structure ProofGeneral : PROOFGENERAL =
    fun restart () =
      let val _ = (loaded_thys := !initial_loaded_thys)
          val _ = (retracted_files := [])
-	 val _ = (kill_goal ())
       in
          (list_loaded_files();
           clear_response_buffer();
+	  (* The goals output from this command is ignored because
+             its followed by an urgent message. *)
+	  kill_goal();	
           writeln "Isabelle Proof General: Isabelle process ready!")
       end;
 
@@ -386,7 +395,7 @@ ml_prompts ">\250" "-\251"; (* ?\372, ?\373 *)
 
 
 (* Wake up, Proof General! *)
-hack_send_prompt();
+(* hack_send_prompt(); *)
 
 (* Get Proof General to cache the loaded files.  *)
 ProofGeneral.restart();
diff --git a/isa/isa.el b/isa/isa.el
index 2b87a5ac..f5d6158f 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -188,6 +188,7 @@ no regular or easily discernable structure."
 
    ;; Some messages delimited by eager annotations
    proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
+   proof-shell-clear-goals-regexp       "Proof General, please clear the goals buffer."
 
    ;; Tested values of proof-shell-eager-annotation-start: 
    ;; "^\\[opening \\|^###\\|^Reading\\|^Proof General\\|^Not reading"
@@ -260,10 +261,16 @@ This is a hook function for proof-activate-scripting-hook."
       ;; Send a use_thy command if there is a corresponding .thy file.
       ;; Let Isabelle do the work of checking whether any work needs
       ;; doing.  Really this should be force_use_thy, too.
-      (proof-shell-invisible-command
-       (format isa-usethy-notopml-command
-	       (file-name-sans-extension buffer-file-name))
-       t)
+      ;; Wait after sending, so that queue is cleared for further commands.
+      ;; (there would be no harm in letting the queue be extended
+      ;; if it were allowed for).
+      (progn
+	(proof-shell-invisible-command
+	 (format isa-usethy-notopml-command
+		 (file-name-sans-extension buffer-file-name))
+	 t)
+	;; Leave the messages from the use around.
+	(setq proof-shell-erase-response-flag nil))
     ))
 
 (defun isa-shell-compute-new-files-list (str)