p-s-classify-output -> p-s-handle-output, and simplify system-specific hook

3 files changed, 33 insertions, 29 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index 4f6d8ece..71a1b7e3 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1683,22 +1683,26 @@ before returning to the top level."
   :type '(repeat function)
   :group 'proof-shell)
 
-(defcustom proof-shell-classify-output-system-specific nil
+(defcustom proof-shell-handle-output-system-specific nil
   "Set this variable to handle system specific output.
-Errors, start of proofs, abortions of proofs and completions of
-proofs are recognised in the function `proof-shell-classify-output'.
-All other output from the proof engine is simply reported to the
-user in the RESPONSE buffer.
-
-To catch further special cases, set this variable to a pair of
-functions '(condf . actf).  Both are given (cmd string) as arguments.
-`cmd' is a string containing the currently processed command.
-`string' is the response from the proof system.  To change the
-behaviour of `proof-shell-classify-output', (condf cmd string) must
-return a non-nil value.  Then (actf cmd string) is invoked.
-
-See the documentation of `proof-shell-classify-output' for the required
-output format."
+Errors and interrupts are recognised in the function  
+`proof-shell-handle-immediate-output'.  Later output is
+handled by `proof-shell-handle-delayed-output', which
+displays messages to the user in *goals* and *response*
+buffers.
+
+This hook can run between the two stages to take some effect.
+
+It should be a function which is passed (cmd string) as
+arguments, where `cmd' is a string containing the currently
+processed command and `string' is the response from the proof
+system.  If action is taken and goals/response display should
+be prevented, the function should update the variable 
+`proof-shell-last-output-kind' to some non-nil symbol.
+
+The symbol will be compared against standard ones, see documentation
+of `proof-shell-last-output-kind'.  A suggested canonical non-standard
+symbol is 'systemspecific."
   :type '(repeat function)
   :group 'proof-shell)
 
diff --git a/lego/lego.el b/lego/lego.el
index be48be41..dfec529f 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -44,12 +44,12 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Users should not need to change this.
 
-(defvar lego-shell-classify-output
-  '((lambda (cmd string) (proof-string-match "^Module" cmd)) .
-    (lambda (cmd string)
-      (setq proof-shell-delayed-output
-	    ;;FIXME: This should be displayed in the minibuffer only
-	    (cons 'insert "\n\nImports done!"))))
+(defvar lego-shell-handle-output
+  '(lambda (cmd string) 
+      (when (proof-string-match "^Module" cmd)
+	;; prevent output and just give a minibuffer message
+	(setq proof-shell-last-output-kind 'systemspecific)
+	(message "Imports done!")))
   "Acknowledge end of processing import declarations.")
 
 (defconst lego-process-config
@@ -396,7 +396,7 @@ For LEGO, we assume that module identifiers coincide with file names."
 	proof-shell-init-cmd lego-process-config
 	proof-shell-restart-cmd lego-process-config
 	pg-subterm-anns-use-stack nil
-	proof-shell-classify-output-system-specific lego-shell-classify-output
+	proof-shell-handle-output-system-specific lego-shell-handle-output
 	lego-shell-current-line-width nil
 
 	;; LEGO uses Unicode escape prefix: liable to create problems
diff --git a/plastic/plastic.el b/plastic/plastic.el
index 2fceda64..09f7b9f2 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -49,12 +49,12 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Users should not need to change this.
 
-(defvar plastic-shell-process-output
-  '((lambda (cmd string) (proof-string-match "^Module" cmd)) .
-    (lambda (cmd string)
-      (setq proof-shell-delayed-output
-	    ;;FIXME: This should be displayed in the minibuffer only
-	    (cons 'insert "\n\nImports done!"))))
+(defvar lego-shell-handle-output
+  '(lambda (cmd string) 
+      (when (proof-string-match "^Module" cmd)
+	;; prevent output and just give a minibuffer message
+	(setq proof-shell-last-output-kind 'systemspecific)
+	(message "Imports done!")))
   "Acknowledge end of processing import declarations.")
 
 (defconst plastic-process-config
@@ -473,7 +473,7 @@ For Plastic, we assume that module identifiers coincide with file names."
 	proof-shell-init-cmd plastic-process-config
 	proof-shell-restart-cmd plastic-process-config
 	pg-subterm-anns-use-stack nil
-	proof-shell-classify-output-system-specific plastic-shell-process-output
+	proof-shell-handle-output-system-specific plastic-shell-handle-output
 	plastic-shell-current-line-width nil
 
 	proof-shell-process-file