Add interactive input setting, and extra flags for action.

3 files changed, 44 insertions, 6 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index f3aea42c..3fbc4680 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -2011,6 +2011,21 @@ list between values for `proof-buffer-syntactic-context' and strings."
   :type '(or string (list (cons (choice 'nil 'string 'comment)  string)))
   :group 'proof-shell)
 
+;; A feature that could be added to support Isabelle's tracing of
+;; tactics.  Seems to be little used, so probably not worth adding.
+;(defcustom proof-shell-interactive-input-regexp nil
+;  "Matches special interactive input request prompt from the prover.
+;A line which matches this regexp  but would otherwise be treated
+;as an ordinary response is instead treated as a prompt for
+;input to be displayed in the minibuffer.  The line which is
+;input is delivered directly to the proof assistant.
+
+;This can be used if the proof assistant requires return key
+;presses to continue, or similar."
+;  :type 'string
+;  :group 'proof-shell)
+
+
 (defcustom proof-shell-trace-output-regexp nil
   "Matches tracing output which should be displayed in trace buffer.
 Each line which matches this regexp but would otherwise be treated
@@ -2116,6 +2131,8 @@ suggests what class of command is about to be inserted:
  'proof-done-invisible	     A non-scripting command
  'proof-done-advancing	     A \"forward\" scripting command
  'proof-done-retracting	     A \"backward\" scripting command
+ 'init-cmd		     Initialization command sent to prover
+ 'interactive-input	     Special interactive input direct to prover
 
 Caveats: You should be very careful about setting this hook.  Proof
 General relies on a careful synchronization with the process between
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 8e65298d..222bb69d 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -690,7 +690,7 @@ NAME does not need to be unique."
 
 (defun pg-set-span-helphighlights (span &optional nohighlight)
   "Set the help echo message, default highlight, and keymap for SPAN."
-  (let ((helpmsg (concat (pg-span-name span) " region")))
+  (let ((helpmsg (concat (pg-span-name span) ""))) ;;   " region"
     (set-span-property span 'balloon-help helpmsg)
     (if pg-show-hints ;; only message in minibuf if hints on
 	(set-span-property 
@@ -700,8 +700,8 @@ NAME does not need to be unique."
 	   helpmsg
 	   " ("
 	   (if (span-property span 'idiom)
-	       "with point in region, use \\[pg-toggle-visibility]  to show/hide; ")
-	   "use \\[popup-mode-menu] for menu)"))))
+	       "with point in region, \\[pg-toggle-visibility] to show/hide; ")
+	   "\\[popup-mode-menu] for menu)"))))
     (set-span-property span 'keymap pg-span-context-menu-keymap)
     (unless nohighlight
       (set-span-property span 'mouse-face 'proof-mouse-highlight-face))))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index cdd4bbfd..f6bd446c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1119,9 +1119,9 @@ The return value is non-nil if the action list is now empty."
 	    nil)))))
 
 (defun proof-shell-insert-loopback-cmd  (cmd)
-  "Insert command sequence triggered by the proof process
-at the end of locked region (after inserting a newline and indenting).
-Assume proof-script-buffer is active."
+  "Insert command sequence sent from prover into script buffer.
+String is inserted at the end of locked region, after a newline 
+and indentation.  Assumes proof-script-buffer is active."
   (unless (string-match "^\\s-*$" cmd)	; FIXME: assumes cmd is single line
     (save-excursion
       (set-buffer proof-script-buffer) 
@@ -1171,6 +1171,15 @@ If none of these apply, display MESSAGE.
 MESSAGE should be a string annotated with 
 `proof-shell-eager-annotation-start', `proof-shell-eager-annotation-end'."
     (cond
+     ;; A feature that could be added to support Isabelle's tracing of
+     ;; tactics.  Seems to be little used, so probably not worth adding.
+     ;;; CASE interactive input regexp: minibuffer prompt for user
+     ;;; FIXME: move this case lower down, for now it clashes with
+     ;;; tracing output in Isabelle
+     ;((and proof-shell-interactive-input-regexp
+     ;	   (string-match proof-shell-interactive-input-regexp message))
+     ;(proof-shell-minibuffer-urgent-interactive-input message))
+
      ;; CASE tracing output: output in the tracing buffer instead
      ;; of the response buffer
      ((and proof-shell-trace-output-regexp
@@ -1364,6 +1373,18 @@ MESSAGE should be a string annotated with
 	   stripped)
 	 'proof-eager-annotation-face)))))
 
+(defvar proof-shell-minibuffer-urgent-interactive-input-history nil)
+
+(defun proof-shell-minibuffer-urgent-interactive-input (msg)
+  "Issue MSG as a prompt and receive user input."
+  (let ((input
+	 (ignore-errors
+	   (read-input 
+	    msg 
+	    nil 
+	    'proof-shell-minibuffer-urgent-interactive-input-history))))
+    ;; Always send something, even if read-input was errorful
+    (proof-shell-insert (or input "") 'interactive-input)))
 
 
 (defun proof-shell-process-urgent-messages ()