diff options
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 73 |
1 files changed, 39 insertions, 34 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 3db7bfde..d8807940 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1,6 +1,6 @@ ;;; proof-script.el --- Major mode for proof assistant script files. ;; -;; Copyright (C) 1994-2009 LFCS Edinburgh. +;; Copyright (C) 1994-2010 LFCS Edinburgh. ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, ;; Thomas Kleymann and Dilip Sequeira ;; License: GPL (GNU GENERAL PUBLIC LICENSE) @@ -309,7 +309,7 @@ value of proof-locked span." (defun proof-script-clear-queue-spans-on-error (badspan) "Remove the queue span from buffer, cleaning spans no longer queued. -If BADSPAN is non-nil, assume that this was the span whose command +If BADSPAN is non-nil, assume that this was the span whose command caused the error. Go to the start of it if `proof-follow-mode' is 'locked. @@ -324,7 +324,7 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}." (goto-char (span-start badspan)) (skip-chars-forward " \t\n")) (when proof-sticky-errors - (pg-set-span-helphighlights badspan + (pg-set-span-helphighlights badspan 'proof-script-highlight-error-face 'proof-script-sticky-error-face))) (proof-script-delete-spans start end))) @@ -496,7 +496,7 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'." (span-detach span) ;; delete overlay, without pre-del fn (remhash id elts)))) -(defun pg-get-element (idiomsym id) +(defun pg-get-element (idiomsym id) "Return proof script element of type IDIOM identifier ID. IDIOM is a symbol, ID is a string." (assert (symbolp idiomsym)) @@ -525,15 +525,15 @@ It is recorded in the span with the 'rawname property." (rawname name) (name (or name id)) (idiom (symbol-name idiomsym)) - (delfn `(lambda () (pg-remove-element + (delfn `(lambda () (pg-remove-element (quote ,idiomsym) (quote ,idsym)))) (elts (cdr-safe (assq idiomsym pg-script-portions)))) (unless elts - (setq pg-script-portions + (setq pg-script-portions (cons (cons idiomsym (setq elts (make-hash-table))) pg-script-portions))) (if (gethash idsym elts) - (proof-debug "Element named " name + (proof-debug "Element named " name " (type " idiom ") was already in buffer.")) (puthash idsym span elts) ;; Idiom and ID are stored in the span as symbols; name as a string. @@ -575,7 +575,7 @@ It is recorded in the span with the 'rawname property." (defun pg-toggle-element-span-visibility (span) "Toggle visibility of SPAN." - (span-set-property + (span-set-property span 'invisible (not (span-property span 'invisible)))) @@ -670,10 +670,10 @@ This is used to annotate the buffer with the result of proof steps." proof-shell-last-output)))) ;; HACK: for Isabelle which puts ugly leading \n's around proofstate. - (if (and (> (length text) 0) + (if (and (> (length text) 0) (string= (substring text 0 1) "\n")) (setq text (substring text 1))) - (if (and (> (length text) 0) + (if (and (> (length text) 0) (string= (substring text -1) "\n")) (setq text (substring text 0 -1))) @@ -703,12 +703,12 @@ Argument FACE means add regular face property FACE to the span." (span-set-property newspan 'pghelp t) (span-set-property newspan 'response output) - (span-set-property newspan 'help-echo + (span-set-property newspan 'help-echo (if (<= (length output) 2) (pg-span-name span) - output)) + output)) - ;; Here's the message we used to show in minibuffer + ;; Here's the message we used to show in minibuffer ;; when pg-show-hints was on: ;; ;; " (" @@ -722,7 +722,7 @@ Argument FACE means add regular face property FACE to the span." (span-set-property newspan 'modification-hooks (list 'pg-delete-self-modification-hook)) (if (or (facep mouseface) - (setq mouseface + (setq mouseface (unless mouseface 'proof-mouse-highlight-face))) (span-set-property newspan 'mouse-face mouseface)) (if face @@ -828,7 +828,7 @@ proof assistant and Emacs has a modified buffer visiting the file." 'wait)))))) (defun proof-query-save-this-buffer-p () - "Predicate testing whether save-some-buffers during scripting should query." + "Predicate testing whether `save-some-buffers' during scripting should query." (and (eq major-mode proof-mode-for-script) (not (eq (current-buffer) proof-script-buffer)))) @@ -1404,7 +1404,7 @@ Argument SPAN has just been processed." (and proof-save-with-hole-regexp (proof-string-match proof-save-with-hole-regexp cmd) ;; Give a message of a name if one can be determined - (proof-minibuffer-message + (proof-minibuffer-message (format "proved %s" (setq nam (if (stringp proof-save-with-hole-result) @@ -1469,7 +1469,7 @@ Argument SPAN has just been processed." (if proof-last-theorem-dependencies (proof-depends-process-dependencies nam gspan))))) -(defun proof-make-goalsave +(defun proof-make-goalsave (gspan goalend savestart saveend nam &optional nestedundos) "Make new goal-save span, using GSPAN. Subroutine of `proof-done-advancing-save'. Argument GOALEND is the end of the goal;." @@ -1578,7 +1578,7 @@ Subroutine of `proof-done-advancing-save'." ;; Hidable regions for commands: the problem is that they have no ;; natural surrounding region, so makes it difficult to define a ;; region for revealing again. - (cond + (cond ((funcall proof-goal-command-p span) (pg-add-element 'statement id bodyspan) (incf proof-nesting-depth)) @@ -1604,7 +1604,7 @@ Subroutine of `proof-done-advancing-save'." (defun proof-segment-up-to-parser (pos &optional next-command-end) "Parse the script buffer from end of queue/locked region to POS. This partitions the script buffer into contiguous regions, classifying -them by type. We Return a list of lists of the form +them by type. Return a list of lists of the form (TYPE TEXT ENDPOS) @@ -1650,7 +1650,7 @@ to the function which parses the script segment by segment." ((null type)) ; nothing left in buffer (t (error - "Proof-segment-up-to-parser: bad TYPE value from proof-script-parse-function."))) + "Proof-segment-up-to-parser: bad TYPE value from proof-script-parse-function"))) ;; (if seg (progn @@ -1781,7 +1781,7 @@ to the function which parses the script segment by segment." (progn (goto-char end) 'cmd))))) -(defun proof-semis-to-vanillas (semis) +(defun proof-semis-to-vanillas (semis &optional queueflags) "Create vanilla spans for SEMIS and a list for the queue. Proof terminator positions SEMIS has the form returned by the function `proof-segment-up-to'. The argument list is destroyed. @@ -1789,7 +1789,9 @@ The callback in each queue element is `proof-done-advancing'. If the variable `proof-script-preprocess' is set (to the name of a function, call that function to construct the first element of -each queue item." +each queue item. + +The optional QUEUEFLAGS are added to each queue item." (let ((start (proof-queue-or-locked-end)) (file (or (buffer-file-name) (buffer-name))) (cb 'proof-done-advancing) @@ -1804,7 +1806,7 @@ each queue item." (let* ((cmd (nth 1 semi)) (qcmd (if proof-script-preprocess (funcall proof-script-preprocess - file + file ;; ignore spaces at start of command (+ start (save-excursion (goto-char start) @@ -1818,7 +1820,8 @@ each queue item." ;; ignored text (span-set-property span 'type 'comment) (setq alist - (cons (list span nil cb) alist))) ; nil was `proof-no-command' + (cons (list span nil cb queueflags) ; nil was `proof-no-command' + alist))) (setq start end))) (nreverse alist))) @@ -1849,20 +1852,20 @@ Assumes that point is at the end of a command." ;; commands, and the adds the commands into the queue. ;; -(defun proof-assert-until-point () +(defun proof-assert-until-point (&optional displayflags) "Process the region from the end of the locked-region until point." (if (proof-only-whitespace-to-locked-region-p) (error "At end of the locked region, nothing to do to!")) (let ((semis (save-excursion - (skip-chars-backward " \t\n" + (skip-chars-backward " \t\n" (proof-queue-or-locked-end)) (proof-segment-up-to-using-cache (point))))) (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis))) (if (null semis) ; maybe inside a string or something. (error "I can't find any complete commands to process!")) - (proof-assert-semis semis))) + (proof-assert-semis semis displayflags))) (defun proof-assert-electric-terminator () "Insert the proof command terminator, and assert up to it. @@ -1882,7 +1885,7 @@ comment, and insert or skip to the next semi)." (= (char-after (point)) proof-terminal-char))) (insert proof-terminal-string) (setq ins t)) - (let* ((pos + (let* ((pos (if proof-electric-terminator-noterminator (1- (point)) (point))) (semis (save-excursion @@ -1899,7 +1902,7 @@ comment, and insert or skip to the next semi)." (proof-assert-semis semis) (proof-script-next-command-advance)))))) -(defun proof-assert-semis (semis) +(defun proof-assert-semis (semis &optional displayflags) "Add to the command queue the list SEMIS of command positions. SEMIS must be a non-empty list, in reverse order (last position first). We assume that the list is contiguous and begins at (proof-queue-or-locked-end). @@ -1909,7 +1912,7 @@ that these may be overwritten)." (proof-activate-scripting nil 'advancing) (let ((startpos (proof-queue-or-locked-end)) (lastpos (nth 2 (car semis))) - (vanillas (proof-semis-to-vanillas semis))) + (vanillas (proof-semis-to-vanillas semis displayflags))) (proof-script-delete-secondary-spans startpos lastpos) (proof-extend-queue lastpos vanillas))) @@ -1957,7 +1960,7 @@ No effect if prover is busy." (span-set-property span 'type 'pbp) (span-set-property span 'cmd cmd) (proof-start-queue (proof-unprocessed-begin) (point) - (list (list span (list cmd) + (list (list span (list cmd) 'proof-done-advancing))))) ;;;###autoload @@ -2174,10 +2177,10 @@ command." (proof-goto-end-of-locked) (backward-char) (setq span (span-at (point) 'type))) - (if span + (if span (proof-retract-target span delete-region) ;; something wrong - (proof-debug + (proof-debug "proof-retract-until-point: couldn't find a span!")))))) @@ -2224,7 +2227,7 @@ command." (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t)) ;; NB: proof-mode-map declared above -(proof-menu-define-keys proof-mode-map) +(proof-menu-define-keys proof-mode-map) (proof-eval-when-ready-for-assistant (define-key proof-mode-map [(control c) (control a)] (proof-ass keymap))) @@ -2644,6 +2647,8 @@ Choice of function depends on configuration setting." 'proof-script-after-change-function nil t)) + + (provide 'proof-script) ;;; proof-script.el ends here |