From 824d1285e74c2d1f54c2d2d789a81452e925e59e Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 17 Nov 1999 16:08:53 +0000 Subject: Added some new code from another patch, but commented out for now. --- generic/proof-shell.el | 37 ++++++++++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) (limited to 'generic') diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 1b2671f9..7d232a5e 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1698,6 +1698,42 @@ in some cases. May be called by proof-shell-invisible-command." Calls proof-state-change-hook." (run-hooks 'proof-state-change-hook)) +; new code to go in after 3.0 +;(defun proof-shell-done-invisible (&optional span) +; "Callback for proof-shell-invisible-command. +;Calls proof-state-change-hook." +; (run-hooks 'proof-state-change-hook) +; (remove-hook 'proof-shell-handle-error-or-interrupt-hook +; 'proof-shell-invisible-hook-fn)) +;; Seems to be hard to write this stuff without a temporary variable +;; (or higher-order functions, sob). +;(defun proof-shell-invisible-hook-fn () +; "Temporary function holding hook for proof-shell-invisible-command.") + +;(defmacro proof-shell-invisible-failure-msg (errormsg) +; "Construct a value for `proof-shell-handle-error-or-interrupt-hook'. +;Give error message ERRORMSG, then remove self from queue." +; `(lambda () +; (proof-shell-done-invisible) +; (error ,(eval errormsg)))) + +;(defmacro proof-shell-invisible-failure-fn (fn) +; "Construct a value for `proof-shell-handle-error-or-interrupt-hook'. +;Call function fn, then remove self from queue." +; `(lambda () +; (proof-shell-done-invisible) +; (,(eval fn)))) +; +; extra arg ERRORMSGFN to proof-shell-invisible-command: +; +;If ERRORMSGFN is non-nil, if the command leads to an error or interrupt +;in the proof assistant, we will give an error. If ERRORMSGFN +;is a string, (error ERRORMSGFN) is called; if ERRORMSGFN is a function, +;it is called directly. If ERRORMSGFN is not a string or function, +;we will give standard error messages for interrupts and errors." +; +; Other (sensible) possibility is to call +; proof-shell-handle-error-or-interrupt-hook with span as argument. (defun proof-shell-invisible-command (cmd &optional wait) "Send CMD to the proof process. Add terminal string if necessary. @@ -1718,7 +1754,6 @@ If WAIT is an integer, wait for that many seconds afterwards." - ;; ;; Proof General shell mode definition -- cgit v1.2.3