diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 42 | ||||
| -rw-r--r-- | generic/proof-shell.el | 48 |
2 files changed, 54 insertions, 36 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 8f98033d..506fa692 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -647,7 +647,7 @@ If a function, it should return the command string to insert." (defcustom proof-terminal-char nil "Character which terminates a command in a script buffer. -You must set this variable." +You must set this variable in script mode configuration." :type 'character :group 'proof-script) @@ -1273,23 +1273,37 @@ to do syntax highlighting with font-lock." "Hooks run by proof-shell-insert before inserting a command. Can be used to configure the proof assistant to the interface in various ways -- for example, to observe or alter the commands sent to -the prover, or to sneak in extra commands to configure the -prover (LEGO uses this to set the pretty printer's line width if -the window width has changed). +the prover, or to sneak in extra commands to configure the prover. This hook is called inside a save-excursion with the proof-shell-buffer current, just before inserting and sending the text in the -variable STRING. The hook can massage STRING or insert additional +variable `string'. The hook can massage `string' or insert additional text directly into the proof-shell-buffer. -Before sending STRING, it will be stripped of carriage returns. - -NB: You should be very careful about setting this hook. Proof General -relies on a careful synchronization with the process between inputs -and outputs. It expects to see a prompt for each input it sends from -the queue. If you add extra input here and it causes more prompts -than expected, things will break! Massaging the variable STRING -may be safer since it is stripped of carriage returns -before being sent." +Before sending `string', it will be stripped of carriage returns. + +Additionally, the hook can examine the variable `action'. It will be +a symbol, set to the callback command which is executed in the proof +shell filter once `string' has been processed. The `action' variable +suggests what class of command is about to be inserted: + + 'proof-shell-done-invisible A non-scripting command + 'proof-done-advancing A \"forward\" scripting command + 'proof-done-retracting A \"backward\" scripting command + +Caveats: You should be very careful about setting this hook. Proof +General relies on a careful synchronization with the process between +inputs and outputs. It expects to see a prompt for each input it +sends from the queue. If you add extra input here and it causes more +prompts than expected, things will break! Extending the variable +`string' may be safer than inserting text directly, since it is +stripped of carriage returns before being sent. + +Example uses: +LEGO uses this hook for setting the pretty printer width if +the window width has changed; +Plastic uses it to remove literate-style markup from `string'. +The x-symbol support uses this hook to convert special characters +into tokens for the proof assistant." :type '(repeat function) :group 'proof-shell) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 60eef074..4b9acb78 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -63,7 +63,7 @@ Set in proof-shell-mode.") (defvar proof-action-list nil "A list of - (SPAN,COMMAND,ACTION) + (SPAN COMMAND ACTION) triples, which is a queue of things to do. See the functions `proof-start-queue' and `proof-exec-loop'.") @@ -1066,9 +1066,9 @@ assistant." (t (setq proof-shell-delayed-output (cons 'insert string))))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Low-level commands for shell communication ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Low-level commands for shell communication +;; (defvar proof-shell-insert-space-fudge (cond @@ -1079,25 +1079,23 @@ assistant." Allows for a difference between different versions of comint across different Emacs versions.") -(defun proof-shell-insert (string) +(defun proof-shell-insert (string action) "Insert STRING at the end of the proof shell, call comint-send-input. -First call proof-shell-insert-hook. Then strip STRING of carriage -returns before inserting it and updating proof-marker to point to -the end of the newly inserted text. -NB: This means that any output received up til now but not -processed by the proof-shell-filter will be lost! We must be -careful to synchronize with the process. This function is used -particularly in proof-start-queue and proof-shell-exec-loop." + +First call proof-shell-insert-hook. The argument ACTION may be +examined by the hook to determine how to process the STRING variable. + +Then strip STRING of carriage returns before inserting it and updating +proof-marker to point to the end of the newly inserted text. + +Do not use this function directly, or output will be lost. It is only +used in proof-append-alist when we start processing a queue, and in +proof-shell-exec-loop, to process the next item." (save-excursion (set-buffer proof-shell-buffer) (goto-char (point-max)) - - ;; Lego uses this hook for setting the pretty printer - ;; width, Coq uses it for sending an initialization string - ;; (although it could presumably use proof-shell-init-cmd?). - ;; Plastic uses it to remove literate-style markup from 'string'. - ;; x-symbol mode uses this hook to convert special characters into - ;; tokens for the proof assistant. + + ;; See docstring for this hook (run-hooks 'proof-shell-insert-hook) ;; Now we replace CRs from string with spaces. This was done in @@ -1120,7 +1118,13 @@ particularly in proof-start-queue and proof-shell-exec-loop." (incf i))) (insert string) + + ;; Advance the proof-marker. This means that any output received + ;; up til now but not processed by the proof-shell-filter will be + ;; lost! We must be careful to synchronize with the process + ;; before using proof-shell-insert. (set-marker proof-marker (point)) + ;; FIXME da: this space fudge is actually a visible hack: ;; the response string begins with a space and a newline. (insert proof-shell-insert-space-fudge) @@ -1171,7 +1175,7 @@ Returns the possibly shortened list." (proof-grab-lock queuemode) (setq proof-shell-delayed-output (cons 'insert "Done.")) (setq proof-action-list alist) - (proof-shell-insert (nth 1 item))))))) + (proof-shell-insert (nth 1 item) (nth 2 item))))))) (defun proof-start-queue (start end alist) "Begin processing a queue of commands in ALIST. @@ -1238,7 +1242,7 @@ The return value is non-nil if the action list is now empty." ;; indicate finished t) ;; Otherwise send the next command to the process - (proof-shell-insert (nth 1 item)) + (proof-shell-insert (nth 1 item) (nth 2 item)) ;; indicate not finished nil))))) @@ -1671,7 +1675,7 @@ By default, let the command be processed asynchronously. But if optional WAIT command is non-nil, wait for processing to finish before and after sending the command." (if wait (proof-shell-wait)) - (proof-shell-ready-prover) + (proof-shell-ready-prover) ; start proof assistant; set vars. (if (not (string-match proof-re-end-of-cmd cmd)) (setq cmd (concat cmd proof-terminal-string))) (proof-start-queue nil nil |