diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-indent.el | 1 | ||||
| -rw-r--r-- | generic/proof-shell.el | 25 | ||||
| -rw-r--r-- | generic/proof-toolbar.el | 4 |
3 files changed, 21 insertions, 9 deletions
diff --git a/generic/proof-indent.el b/generic/proof-indent.el index 4cf14084..1caeaadb 100644 --- a/generic/proof-indent.el +++ b/generic/proof-indent.el @@ -45,6 +45,7 @@ (t (cond ((eq c ?\() (cond + ;; FIXME broken: comment strings are not generic. ((looking-at "(\\*") (progn (incf comment-level) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index ede3f76d..437f3e55 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -60,7 +60,12 @@ Set in proof-shell-mode.") (defvar proof-marker nil "Marker in proof shell buffer pointing to previous command input.") -(defvar proof-action-list nil "action list") +(defvar proof-action-list nil + "A list of + + (span,command,action) + +triples, which is a queue of things to do.") @@ -132,7 +137,7 @@ Set in proof-shell-mode.") (defun proof-shell-ready-prover () "Make sure the proof assistant is ready for a command" - (proof-start-shell) + (proof-shell-start) (if proof-shell-busy (error "Proof Process Busy!"))) (defun proof-shell-live-buffer () @@ -174,11 +179,12 @@ No error messages. Useful as menu or toolbar enabler." ;; Starting and stopping the proof shell ;; -(defun proof-start-shell () +(defun proof-shell-start () "Initialise a shell-like buffer for a proof assistant. Also generates goal and response buffers. Does nothing if proof assistant is already running." + (interactive) (if (proof-shell-live-buffer) () (run-hooks 'proof-pre-shell-start-hook) @@ -353,10 +359,12 @@ and clearing all script buffers." (incf a)) (apply 'concat (nreverse ls)))) +;; FIXME da: this is an oddity. Was bound by default to +;; control - button1, I've turned it off. (defun proof-send-span (event) (interactive "e") (let* ((span (span-at (mouse-set-point event) 'type)) - (str (span-property span 'cmd))) + (str (if span (span-property span 'cmd)))) (cond ((and (eq (current-buffer) proof-script-buffer) (not (null span))) (proof-goto-end-of-locked) @@ -1017,11 +1025,11 @@ if none of these apply, display." 'proof-eager-annotation-face)))) (defvar proof-shell-urgent-message-marker nil - "Marker in proof shell buffer used for parsing urgent messages.") + "Marker in proof shell buffer pointing to end of last urgent message.") (defun proof-shell-process-urgent-messages () "Scan the shell buffer for urgent messages. -Scanning starts from proof-shell-urgent-message-pos and processes +Scanning starts from proof-shell-urgent-message-marker and processes strings between eager-annotation-start and eager-annotation-end." (let ((pt (point))) (goto-char @@ -1051,9 +1059,10 @@ strings between eager-annotation-start and eager-annotation-end." ;; FIXME da: moreover, are urgent messages full processed?? ;; some seem to get dumped in response buffer. -(defun proof-shell-filter (str) +(defun proof-shell-filter (str) "Filter for the proof assistant shell-process. -We sleep until we get a wakeup-char in the input, then run +We process urgent messages first. Then wait until we get a +proof-shell-wakeup-char in the input, then run proof-shell-process-output, and set proof-marker to keep track of how far we've got." (save-excursion diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index 44c37a9e..4ce86a4f 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -1,6 +1,7 @@ ;; proof-toolbar.el Toolbar for Proof General ;; -;; David Aspinall <da@dcs.ed.ac.uk> +;; Copyright (C) 1998 David Aspinall. +;; Author: David Aspinall <da@dcs.ed.ac.uk> ;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> ;; ;; $Id$ @@ -353,6 +354,7 @@ Move point if the end of the locked position is invisible." ) (defun proof-toolbar-restart () + "Restart scripting via proof-shell-restart." (interactive) (if (proof-toolbar-restart-enable-p) (proof-shell-restart))) |