Fixes to debug long standing not-showing-first-goal problem.

3 files changed, 17 insertions, 17 deletions

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index 0e5eace5..09ecc7ab 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -133,6 +133,7 @@ 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();
@@ -377,10 +378,12 @@ in
   fun print_current_goals_with_plain_output i j t =
     Library.setmp prs_fn out (print_current_goals_default i j) t;
 
-(* Annoyingly, Proof General waits for the first prompt before doing
-  anything.  Hack sending a prompt to get things going *)
+(* Proof General has problems sending commands outside of the
+   action list.  Also, it waits for the first prompt before doing
+   anything.  The next function hacks sending a prompt to get
+   things going and to help fix things later. *)
 
- val _ = out ">\250 \n";
+  fun hack_send_prompt _ = out ">\250 \n";
 end;
 
 print_current_goals_fn := print_current_goals_with_plain_output;
@@ -391,7 +394,6 @@ print_current_goals_fn := print_current_goals_with_plain_output;
 ml_prompts ">\250" "-\251"; (* ?\372, ?\373 *)
 
 
-
 (*
    NB: Obscure bug with proof-shell-annotated-prompt-regexp set
    properly to include annotations: PG doesn't recognize first proof
@@ -403,11 +405,9 @@ ml_prompts ">\250" "-\251"; (* ?\372, ?\373 *)
       update_verbose:=true;
    Unfortunately broken.  We use list_loaded_files instead. *)
 
-(* Get Proof General to cache the loaded files.  *)
-
-ProofGeneral.restart();
-
-
-
 
+(* Wake up, Proof General! *)
+hack_send_prompt();
 
+(* Get Proof General to cache the loaded files.  *)
+ProofGeneral.restart();
diff --git a/isa/example.ML b/isa/example.ML
index a8922e87..11b807f4 100644
--- a/isa/example.ML
+++ b/isa/example.ML
@@ -14,6 +14,7 @@ br conjI 1;
 be conjE 1;
 ba 1;
 be conjE 1;
+ba 45;
 ba 1;
 qed "and_comms";
 
diff --git a/isa/isa.el b/isa/isa.el
index 46f2e00d..e25692c7 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -150,7 +150,8 @@ no regular or easily discernable structure."
   (setq
    proof-shell-first-special-char	?\360
 
-   proof-shell-annotated-prompt-regexp   ">\372"
+   proof-shell-wakeup-char		 ?\372
+   proof-shell-annotated-prompt-regexp   "\\(val it = () : unit\n\\)?>\372"
    ;; "^\\(val it = () : unit\n\\)?> "
    ;; non-annotation, with val it's: "^\\(val it = () : unit\n\\)?> "
 
@@ -173,7 +174,6 @@ no regular or easily discernable structure."
    ;; matches subgoal name
    proof-shell-goal-regexp		"\370[ \t]*\\([0-9]+\\)\\."
 
-   proof-shell-wakeup-char		?\372
    proof-shell-start-goals-regexp	"\366"
    proof-shell-end-goals-regexp		"\367"
    proof-shell-goal-char	        ?\370
@@ -183,10 +183,10 @@ no regular or easily discernable structure."
    proof-shell-restart-cmd		"ProofGeneral.restart();"
    proof-shell-quit-cmd			"exit 0;"
    
-   proof-shell-eager-annotation-start   "\360\\|\362\\|\364"
-   proof-shell-eager-annotation-end     "\361\\|\363\\|\365"
+   proof-shell-eager-annotation-start   "\360\\|\362"
+   proof-shell-eager-annotation-end     "\361\\|\363"
 
-   ;; Some messages delineated by eager annotations
+   ;; Some messages delimited by eager annotations
    proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
 
    ;; Tested values of proof-shell-eager-annotation-start: 
@@ -260,8 +260,7 @@ 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.
-      ;; Wait for response from proof assistant before continuing.
-      (proof-shell-insert
+      (proof-shell-invisible-command
        (format isa-usethy-notopml-command
 	       (file-name-sans-extension buffer-file-name))
        t)