Added Isamode-like keybinding C-c C-l for proof-prf.

2 files changed, 17 insertions, 9 deletions

diff --git a/isa/ProofGeneral.ML b/isa/ProofGeneral.ML
index 1663953d..0e5eace5 100644
--- a/isa/ProofGeneral.ML
+++ b/isa/ProofGeneral.ML
@@ -377,10 +377,10 @@ 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 *)
+(* Annoyingly, Proof General waits for the first prompt before doing
+  anything.  Hack sending a prompt to get things going *)
 
-  val _ = out "> \n";
+ val _ = out ">\250 \n";
 end;
 
 print_current_goals_fn := print_current_goals_with_plain_output;
@@ -388,9 +388,11 @@ print_current_goals_fn := print_current_goals_with_plain_output;
 
 (* add specials to ml prompts *)
 
+ml_prompts ">\250" "-\251"; (* ?\372, ?\373 *)
+
+
+
 (*
-   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
    state output.
diff --git a/isa/isa.el b/isa/isa.el
index 8a5421d1..46f2e00d 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -150,8 +150,8 @@ no regular or easily discernable structure."
   (setq
    proof-shell-first-special-char	?\360
 
-   proof-shell-annotated-prompt-regexp   ; ">\372"
-   "^\\(val it = () : unit\n\\)?> "
+   proof-shell-annotated-prompt-regexp   ">\372"
+   ;; "^\\(val it = () : unit\n\\)?> "
    ;; non-annotation, with val it's: "^\\(val it = () : unit\n\\)?> "
 
    ;; This pattern is just for comint, it matches a range of
@@ -181,7 +181,7 @@ no regular or easily discernable structure."
    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-quit-cmd			"exit 0;"
    
    proof-shell-eager-annotation-start   "\360\\|\362\\|\364"
    proof-shell-eager-annotation-end     "\361\\|\363\\|\365"
@@ -260,9 +260,12 @@ 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
        (format isa-usethy-notopml-command
-	       (file-name-sans-extension buffer-file-name)))))
+	       (file-name-sans-extension buffer-file-name))
+       t)
+    ))
 
 (defun isa-shell-compute-new-files-list (str)
   "Compute the new list of files read by the proof assistant.
@@ -314,6 +317,9 @@ proof-included-files-list."
     "Isabelle script" nil
     (isa-mode-config)))
 
+(define-key isa-proofscript-mode-map
+  [(control c) (control l)] 'proof-prf)	; keybinding like Isamode
+