diff options
Diffstat (limited to 'proof.el')
-rw-r--r-- | proof.el | 1363 |
1 files changed, 1038 insertions, 325 deletions
@@ -1,19 +1,68 @@ -;; proof.el Major mode for proof assistants Copyright (C) 1994, -;; 1995, 1996 LFCS Edinburgh. This version by Dilip Sequeira, by -;; rearranging Thomas Schreiber's code. +;; proof.el Major mode for proof assistants +;; Copyright (C) 1994 - 1997 LFCS Edinburgh. +;; Authors: Yves Bertot, Healfdene Goguen, Thomas Kleymann and Dilip Sequeira ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> -;; Time-stamp: <22 Nov 96 tms /home/tms/elisp/proof.el> ;; Thanks to David Aspinall, Robert Boyer, Rod Burstall, ;; James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens +;; TO DO: + +;; o Need to think about fixing up errors caused by pbp-generated commands + +;; o Proof mode breaks if an error is encountered during the import +;; phase. + +;; o proof-undo-last-successful-command needs to be extended so that +;; it deletes regions of the script buffer when invoked outside a proof + +;; o undo support needs to consider Discharge; perhaps unrol to the +;; beginning of the module? + +;; $Log$ +;; Revision 1.11 1997/10/13 17:09:52 tms +;; put script-management branch back on main branch +;; +;; Revision 1.10.2.15 1997/10/10 19:20:01 djs +;; Added multiple file support, changed the way comments work, fixed a +;; few minor bugs, and merged in coq support by hhg. +;; +;; Revision 1.10.2.13 1997/10/07 13:27:51 hhg +;; New structure sharing as much as possible between LEGO and Coq. +;; +;; Revision 1.10.2.12 1997/10/03 14:52:53 tms +;; o Replaced (string= "str" (substring cmd 0 n)) +;; by (string-match "^str" cmd) +;; The latter doesn't raise an exception if cmd is too short +;; +;; o lego-count-undos: now depends on lego-undoable-commands-regexp +;; with special treatment of Equiv +;; +;; Revision 1.10.2.11 1997/09/19 11:23:23 tms +;; o replaced ?\; by proof-terminal-char +;; o fixed a bug in proof-process-active-terminator +;; +;; Revision 1.10.2.10 1997/09/12 12:33:41 tms +;; improved lego-find-and-forget +;; +;; Revision 1.10.2.9 1997/09/11 15:39:19 tms +;; fixed a bug in proof-retract-until-point +;; + (require 'compile) (require 'comint) (require 'etags) +(require 'proof-fontlock) (autoload 'w3-fetch "w3" nil t) -(autoload 'easy-menu-define "easymenu") + +(defmacro deflocal (var value docstring) + (list 'progn + (list 'defvar var 'nil docstring) + (list 'make-variable-buffer-local (list 'quote var)) + (list 'setq var value))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Configuration ;; @@ -27,55 +76,127 @@ process starts up.") ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Variables used by proof mode, all auto-buffer-local ;; +;; Other buffer-local variables used by proof mode ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defmacro deflocal (var &optional value docstring) - (list 'make-variable-buffer-local (list 'quote var)) - (list 'defvar var value docstring)) - ;; These should be set before proof-config-done is called -(deflocal proof-terminal-char) +(defvar proof-terminal-char nil "terminator character") + +(defvar proof-comment-start nil "Comment start") +(defvar proof-comment-end nil "Comment end") + +(defvar proof-save-command-regexp nil "Matches a save command") +(defvar proof-save-with-hole-regexp nil "Matches a named save command") +(defvar proof-goal-command-regexp nil "Matches a goal command") +(defvar proof-goal-with-hole-regexp nil "Matches a saved goal command") + +(defvar proof-undo-target-fn nil "Compute how to undo to this extent") +(defvar proof-forget-target-fn nil "Compute how to forget back to this ext") +(defvar proof-kill-goal-command nil "How to kill a goal.") + +(defvar pbp-change-goal nil + "*Command to change to the goal %s") + +;; these should be set in proof-pre-shell-start-hook + +(defvar proof-prog-name nil "program name for proof shell") +(defvar proof-mode-for-shell nil "mode for proof shell") +(defvar proof-mode-for-pbp nil "The actual mode for Proof-by-Pointing.") +(defvar proof-shell-config nil + "Function to config proof-system to interface") + +(defvar proof-pre-shell-start-hook) +(defvar proof-post-shell-exit-hook) -(make-local-hook 'proof-pre-shell-start-hook) -(make-local-hook 'proof-post-shell-start-hook) +(defvar proof-shell-prompt-pattern nil + "comint-prompt-pattern for proof shell") -(deflocal proof-comment-start) -(deflocal proof-comment-end) +(defvar proof-shell-init-cmd nil + "The command for initially configuring the proof process") -;; these should be set in proof-shell-start-hook +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Generic config for script management ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(deflocal proof-shell-prog-name) -(deflocal proof-shell-process-name) -(deflocal proof-shell-buffer-name) -(deflocal proof-shell-prompt-pattern) -(deflocal proof-shell-mode-is) +(defvar proof-shell-wakeup-char nil + "A character terminating the prompt in annotation mode") -(deflocal proof-shell-abort-goal-regexp nil +(defvar proof-shell-annotated-prompt-regexp "" + "Annotated prompt pattern") + +(defvar proof-shell-abort-goal-regexp nil "*Regular expression indicating that the proof of the current goal has been abandoned.") -(deflocal proof-error-regexp nil +(defvar proof-shell-error-regexp nil "A regular expression indicating that the PROOF process has identified an error.") -(deflocal proof-shell-proof-completed-regexp nil +(defvar proof-shell-proof-completed-regexp nil "*Regular expression indicating that the proof has been completed.") -(deflocal proof-shell-change-goal nil - "*Command to change to the goal %s") +(defvar proof-shell-result-start "" + "String indicating the start of an output from the prover following + a `pbp-goal-command' or a `pbp-hyp-command'.") + +(defvar proof-shell-result-end "" + "String indicating the end of an output from the prover following a + `pbp-goal-command' or a `pbp-hyp-command'.") + +(defvar proof-shell-start-goals-regexp "" + "String indicating the start of the proof state.") -;; Supply these if you want +(defvar proof-shell-end-goals-regexp "" + "String indicating the end of the proof state.") -(make-local-hook 'proof-shell-safe-send-hook) -(make-local-hook 'proof-shell-exit-hook) +(defvar proof-shell-sanitise t "sanitise output?") -;; These get computed in proof-mode-child-config-done +(defvar pbp-error-regexp nil + "A regular expression indicating that the PROOF process has + identified an error.") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Internal variables used by scripting and pbp ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-terminal-string nil + "You are not authorised for this information.") + +(defvar proof-re-end-of-cmd nil + "You are not authorised for this information.") + +(defvar proof-re-term-or-comment nil + "You are not authorised for this information.") + +(defvar proof-locked-hwm nil + "Upper limit of the locked region") -(deflocal proof-terminal-string) -(deflocal proof-re-end-of-cmd) -(deflocal proof-re-term-or-comment) +(defvar proof-queue-loose-end nil + "Limit of the queue region that is not equal to proof-locked-hwm.") + +(defvar proof-mark-ext nil + "You are not authorised for this information.") + +(defvar proof-shell-buffer nil + "You are not authorised for this information.") + +(defvar proof-script-buffer nil + "You are not authorised for this information.") + +(defvar proof-pbp-buffer nil + "You are not authorised for this information.") + +(defvar proof-shell-busy nil + "You are not authorised for this information.") + +(deflocal proof-buffer-type nil + "You are not authorised for this information.") + +(defvar proof-action-list nil "action list") + +(defvar proof-included-files-list nil + "Files currently included in proof process") ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Bridging the emacs19/xemacs gulf ;; @@ -124,6 +245,102 @@ nil (or history 'shell-command-history))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Spans and segments ;; +;; Because one day we might wish to port to emacs19 ;; +;; Note that we need to go back to using marks too ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun make-span (start end) + (make-extent start end)) + +(defun set-span-endpoints (span start end) + (set-extent-endpoints span start end)) + +(defun set-span-start (span value) + (set-extent-endpoints span value (extent-end-position span))) + +(defun set-span-end (span value) + (set-extent-endpoints span (extent-start-position span) value)) + +(defun span-property (span name) + (extent-property span name)) + +(defun set-span-property (span name value) + (set-extent-property span name value)) + +(defun delete-span (span) + (delete-extent span)) + +(defun delete-spans (start end prop) + (mapcar-extents 'delete-extent nil (current-buffer) start end nil prop)) + +(defun span-at (pt prop) + (extent-at pt nil prop)) + +(defun span-at-before (pt prop) + (extent-at pt nil prop nil 'before)) + +(defun span-start (span) + (extent-start-position span)) + +(defun span-end (span) + (extent-end-position span)) + +(defun prev-span (span prop) + (extent-at (extent-start-position span) nil prop nil 'before)) + +(defun next-span (span prop) + (extent-at (extent-end-position span) nil prop nil 'after)) + +(defvar proof-locked-ext nil + "Upper limit of the locked region") + +(defvar proof-queue-ext nil + "Upper limit of the locked region") + +(defun proof-init-segmentation () + (setq proof-queue-loose-end nil) + (setq proof-queue-ext (make-extent nil nil (current-buffer))) + (set-extent-property proof-queue-ext 'start-closed t) + (set-extent-property proof-queue-ext 'end-open t) + (set-extent-property proof-queue-ext 'read-only t) + (make-face 'proof-queue-face) + (if (eq (device-class (frame-device)) 'color) + (set-face-background 'proof-queue-face "mistyrose") + (set-face-background 'proof-queue-face "Black") + (set-face-foreground 'proof-queue-face "White")) + (set-extent-property proof-queue-ext 'face 'proof-queue-face) + + (setq proof-locked-hwm nil) + (setq proof-locked-ext (make-extent nil nil (current-buffer))) + (set-extent-property proof-locked-ext 'start-closed t) + (set-extent-property proof-locked-ext 'end-open t) + (set-extent-property proof-locked-ext 'read-only t) + (if (eq (device-class (frame-device)) 'color) + (progn (make-face 'proof-locked-face) + (set-face-background 'proof-locked-face "lavender") + (set-extent-property proof-locked-ext 'face 'proof-locked-face)) + (set-extent-property proof-locked-ext 'face 'underline))) + +(defun proof-segment-buffer (eol eoq) + (setq proof-locked-hwm eol + proof-queue-loose-end eoq) + (if (and (null eoq) (null eol)) + (progn (detach-extent proof-locked-ext) + (detach-extent proof-queue-ext)) + (if (eq eol (point-min)) + (detach-extent proof-locked-ext) + (set-extent-endpoints proof-locked-ext (point-min) eol + (current-buffer))) + (if (eq eol eoq) + (progn + (detach-extent proof-queue-ext) + (setq proof-queue-loose-end nil)) + (set-extent-endpoints proof-queue-ext eol eoq (current-buffer))))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; A couple of small utilities ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -142,264 +359,762 @@ (string-match (concat "[^" separator "]") s end-of-word-occurence)) separator))))) - - -(defun ids-to-regexp (l) - "transforms a non-empty list of identifiers `l' into a regular - expression matching any of its elements" -(mapconcat (lambda (s) (concat "\\<" s "\\>")) l "\\|")) - (defun w3-remove-file-name (address) "remove the file name in a World Wide Web address" (string-match "://[^/]+/" address) (concat (substring address 0 (match-end 0)) (file-name-directory (substring address (match-end 0))))) -(defun occurence (STRING &optional LOWER-BOUND UPPER-BOUND) - "Counts the number of occurences of STRING in the current buffer - between the positions LOWER-BOUND and UPPER-BOUND. - Optional first argument. nil is equivalent to (point-min). - Optional second argument. nil is equivalent to (point-max)." - (save-excursion - (let ((LOWER-BOUND (or LOWER-BOUND (point-min)))) - (goto-char LOWER-BOUND) - (let ((pos (search-forward STRING UPPER-BOUND t))) - (if pos (+ 1 (occurence STRING pos UPPER-BOUND)) 0))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; A few random hacks ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defun proof-end-of-locked () + "Jump to the end of the locked region." + (interactive) + (or proof-locked-hwm (point-min))) -(defun proof-skip-comments () - (forward-comment (buffer-size)) - (point)) - -; Find the last real semicolon, or point-min, leaving the point after -; the semi and any junk. Returns nil if we seemto be inside a comment - -(defun proof-find-start-of-command () - (if (re-search-backward proof-re-term-or-comment nil t) - (cond ((looking-at proof-terminal-string) - (forward-char) - (proof-skip-comments)) - ((looking-at (substring proof-comment-start 0 1)) nil) - ((looking-at (substring proof-comment-end 0 1)) - (if (search-backward proof-comment-start nil t) - (if (equal (point) (point-min)) - (proof-skip-comments)) - (backward-char) - (proof-find-start-of-command)) - (point))) - (goto-char (point-min)) - (proof-skip-comments))) - - -;; there seems to be some duplication of work here, as one might -;; expect that the functionality of proof-find-end-of-command would be -;; required in proof-process-active-terminator -(defun proof-find-end-of-command (&optional COUNT) - "Move to the end of the command. COUNT-1 end-of-command symbols - `proof-terminal-string' are within comments" +(defun proof-goto-end-of-locked () + "Jump to the end of the locked region." (interactive) - (let ((point (point)) - (pos (search-forward proof-terminal-string nil nil COUNT))) - (and pos - ;; an end of command has been found - ;; is pos within a comment relative to the starting point of - ;; the search? - (> (occurence proof-comment-start point (point)) - (occurence proof-comment-end point (point))) - (goto-char point) - (proof-find-end-of-command (if COUNT (+ 1 COUNT) 2))))) - -(defun proof-shell-process () - (and (stringp proof-shell-process-name) - (get-process proof-shell-process-name))) - -(defun proof-shell-buffer () - (and (stringp proof-shell-buffer-name) - (get-buffer proof-shell-buffer-name))) - -(defun proof-display-buffer (buffer) - (let ((tmp-buffer (current-buffer))) - (display-buffer buffer) - (display-buffer tmp-buffer))) - -(defun proof-append-terminator (string) - (or (and - (string-match proof-re-end-of-cmd string) - string) - (setq string (concat string proof-terminal-string)))) - + (goto-char (proof-end-of-locked))) + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Comint-style stuff: sending input to the process etc ;; +;; Starting and stopping the proof-system shell ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun proof-input-sender (proc string) - "Function to actually send to the PROOF process `proc' the `string' - submitted by the user. It then calls proof-shell-safe-send-hook if safe - to do so." - (comint-simple-send proc string) - (and (string-match proof-re-end-of-cmd string) - (run-hooks 'proof-shell-safe-send-hook))) +(defun proof-shell-live-buffer () + (if (and proof-shell-buffer + (comint-check-proc proof-shell-buffer)) + proof-shell-buffer)) -(defun proof-interrupt-subjob () - (interactive) - (and (proof-shell-process) - (interrupt-process (proof-shell-process)))) - -(defun proof-simple-send (string &optional silent) - "send `string' to the PROOF PROCESS. - If `silent' is enabled then `string' should not be echoed." - (or (proof-shell-process) (proof-start-shell)) - (let ((proof-buf (proof-shell-buffer))) - (if proof-buf +(defun proof-start-shell () + (if (proof-shell-live-buffer) + () + (run-hooks 'proof-pre-shell-start-hook) + (setq proof-included-files-list nil) + (if proof-prog-name-ask-p (save-excursion - (progn - (set-buffer proof-buf) - (goto-char (point-max)) - (if (and proof-shell-echo-input (not silent)) - (progn - (princ string proof-buf) - (comint-send-input)) - (proof-input-sender proof-shell-process-name string) - ))) - (message (format "No active %s process" proof-shell-process-name))))) + (setq proof-prog-name (read-shell-command "Run process: " + proof-prog-name)))) + (let ((proc + (concat "Inferior " + (substring proof-prog-name + (string-match "[^/]*$" proof-prog-name))))) + (while (get-buffer (concat "*" proc "*")) + (if (string= (substring proc -1) ">") + (aset proc (- (length proc) 2) + (+ 1 (aref proc (- (length proc) 2)))) + (setq proc (concat proc "<2>")))) + + (message (format "Starting %s process..." proc)) + + (let ((prog-name-list (string-to-list proof-prog-name " "))) + (apply 'make-comint (append (list proc (car prog-name-list) nil) + (cdr prog-name-list)))) + + (setq proof-shell-buffer (get-buffer (concat "*" proc "*"))) + (setq proof-pbp-buffer (get-buffer-create (concat "*" proc "-goals*"))) -(defun proof-simulate-send-region (point1 point2 &optional terminator) - "Send the area between point1 and point2 to the inferior shell running lego." - (let (str) - (setq str (buffer-substring point1 point2)) - (and terminator (setq str (proof-append-terminator str))) - (proof-simple-send str))) + (save-excursion + (set-buffer proof-shell-buffer) + (funcall proof-mode-for-shell) + (set-buffer proof-pbp-buffer) + (funcall proof-mode-for-pbp)) -;; proof-send-command tries to figure out where commands start and end -;; without having to parse expressions. Actually needs re-writing. + (message + (format "Starting %s process... done." proc))))) + -(defun proof-send-command () - "Send current command to inferior shell." +(defun proof-stop-shell () + "Exit the PROOF process + + Runs proof-shell-exit-hook if non nil" - (interactive) - (let (start end) - (save-excursion - (setq start (proof-find-start-of-command)) - (if start - (setq end (search-forward proof-terminal-string nil t))) - (if (not end) - (setq end (point-max)) - (backward-char)) - (proof-simulate-send-region start end t)))) - -(defun proof-send-line () - "Send current line to inferior shell running proof" (interactive) (save-excursion - (let (start end) - (beginning-of-line 1) - (setq start (point)) - (end-of-line 1) - (setq end (point)) - (proof-simulate-send-region start end))) - (forward-line 1)) - -(defun proof-send-region () - "Sends the current region to the inferior shell running proof and - appends a terminator if neccessary." - (interactive) - (let (start end) - (save-excursion - (setq end (point)) - (exchange-point-and-mark) - (setq start (point))) - (proof-simulate-send-region start end t))) + (let ((buffer (proof-shell-live-buffer)) (proc)) + (if buffer + (progn + (save-excursion + (set-buffer buffer) + (setq proc (process-name (get-buffer-process))) + (comint-send-eof) + (save-excursion + (set-buffer proof-script-buffer) + (proof-segment-buffer nil nil)) + (kill-buffer)) + (run-hooks 'proof-shell-exit-hook) + + ;;it is important that the hooks are + ;;run after the buffer has been killed. In the reverse + ;;order e.g., intall-shell-fonts causes problems and it + ;;is impossible to restart the PROOF shell -(defun proof-command (command &optional silent) - (let ((str (proof-append-terminator command))) - (proof-simple-send str silent))) + (message (format "%s process terminated." proc))))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Starting, stopping, and interrupting the lego shell ;; -;; There maybe more functionality here one day to support multiple ;; -;; subprocesses ;; +;; Proof by pointing ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun proof-start-shell () - (run-hooks 'proof-pre-shell-start-hook) - (let ((proof-buf (and proof-shell-process-name (proof-shell-buffer)))) - (if (comint-check-proc proof-buf) - () - (save-excursion - (and proof-prog-name-ask-p - (setq proof-shell-prog-name - (read-shell-command "Run process: " - proof-shell-prog-name)))) - (or proof-shell-process-name - (setq proof-shell-process-name - (concat - "Inferior " - (substring proof-shell-prog-name - (string-match "[^/]*$" proof-shell-prog-name) - (string-match "$" proof-shell-prog-name))))) - (message (format "Starting %s process..." proof-shell-process-name)) - - (proof-spawn-process proof-shell-prog-name - proof-shell-process-name proof-shell-buffer-name) - (run-hooks 'proof-post-shell-start-hook) - (pbp-goals-init) - (message - (format "Starting %s process... done." proof-shell-process-name))))) - +(defconst pbp-goal-command "Pbp %s;" + "Command informing the prover that `pbp-button-action' has been + requested on a goal.") + + +(defconst pbp-hyp-command "PbpHyp %s;" + "Command informing the prover that `pbp-button-action' has been + requested on an assumption.") + +(defvar pbp-keymap (make-keymap 'Pbp-keymap) + "Keymap for proof mode") + +(defun pbp-button-action (event) + (interactive "e") + (mouse-set-point event) + (pbp-construct-command)) + +(define-key pbp-keymap 'button2 'pbp-button-action) + +; Using the extents in a mouse behavior is quite simple: from the +; mouse position, find the relevant extent, then get its annotation +; and produce a piece of text that will be inserted in the right +; buffer. Attaching this behavior to the mouse is simply done by +; attaching a keymap to all the extents. + +(defun proof-expand-path (string) + (let ((a 0) (l (length string)) ls) + (while (< a l) + (setq ls (cons (int-to-string (aref string a)) + (cons " " ls))) + (incf a)) + (apply 'concat (nreverse ls)))) + +(defun pbp-construct-command () + (let* ((ext (span-at (point) 'proof)) + (top-ext (span-at (point) 'proof-top-element)) + (top-info (span-property top-ext 'proof-top-element)) + path cmd) + (if (extentp top-ext) + (cond + ((extentp ext) + (setq path (concat (cdr top-info) + (proof-expand-path (span-property ext 'proof)))) + (setq cmd + (if (eq 'hyp (car top-info)) + (format pbp-hyp-command path) + (format pbp-goal-command path))) + (pop-to-buffer proof-script-buffer) + (proof-invisible-command cmd)) + (t + (if (eq 'hyp (car top-info)) + (progn + (setq cmd (format pbp-hyp-command (cdr top-info))) + (pop-to-buffer proof-script-buffer) + (proof-invisible-command cmd)) + (setq cmd (format pbp-change-goal (cdr top-info))) + (pop-to-buffer proof-script-buffer) + (proof-insert-pbp-command cmd))))))) -(defun proof-spawn-process (prog-name process-name buffer-name) - "Start a new shell in a new buffer" +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Turning annotated output into pbp goal set ;; +;; All very lego-specific at present ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (set-buffer - (let ((prog-name-list (string-to-list prog-name " "))) - (apply 'make-comint - (append (list process-name - (car prog-name-list) nil) - (cdr prog-name-list))))) +(defvar proof-shell-first-special-char nil "where the specials start") +(defvar proof-shell-goal-char nil "goal mark") +(defvar proof-shell-start-char nil "annotation start") +(defvar proof-shell-end-char nil "annotation end") +(defvar proof-shell-field-char nil "annotated field end") +(defvar proof-shell-eager-annotation-start nil "eager ann. field start") +(defvar proof-shell-eager-annotation-end nil "eager ann. field end") + +(defvar proof-shell-assumption-regexp nil + "A regular expression matching the name of assumptions.") + +(defvar proof-shell-goal-regexp nil + "A regular expressin matching the identifier of a goal.") + +(defvar proof-shell-noise-regexp nil + "Unwanted information output from the proof process within + `proof-start-goals-regexp' and `proof-end-goals-regexp'.") + +(defun pbp-make-top-extent (start end) + (let (extent name) + (goto-char start) + (setq name (cond + ((looking-at proof-shell-goal-regexp) + (cons 'goal (match-string 1))) + ((looking-at proof-shell-assumption-regexp) + (cons 'hyp (match-string 1))))) + (beginning-of-line) + (setq start (point)) + (goto-char end) + (beginning-of-line) + (backward-char) + (setq extent (make-extent start (point))) + (set-span-property extent 'mouse-face 'highlight) + (set-span-property extent 'keymap pbp-keymap) + (set-span-property extent 'proof-top-element name))) + +(defun proof-shell-analyse-structure (string) + (save-excursion + (let* ((ip 0) (op 0) ap (l (length string)) + (ann (make-string (length string) ?x)) + (stack ()) (topl ()) + (out (make-string l ?x )) c ext) + (while (< ip l) + (setq c (aref string ip)) + (if (< c proof-shell-first-special-char) + (progn (aset out op c) + (incf op)) + (cond + ((= c proof-shell-goal-char) + (setq topl (append topl (list (+ 1 op))))) + ((= c proof-shell-start-char) + (setq ap (- (aref string (incf ip)) 32)) + (incf ip) + (while (not (= (aref string ip) proof-shell-end-char)) + (aset ann ap (- (aref string ip) 32)) + (incf ap) + (incf ip)) + (setq stack (cons op (cons (substring ann 0 ap) stack)))) + ((= c proof-shell-field-char) + (setq ext (make-extent (car stack) op out)) + (set-span-property ext 'mouse-face 'highlight) + (set-span-property ext 'keymap pbp-keymap) + (set-span-property ext 'proof (cadr stack)) + (set-span-property ext 'duplicable t) + (setq stack (cddr stack))))) + (incf ip)) + (display-buffer (set-buffer proof-pbp-buffer)) + (erase-buffer) + (insert (substring out 0 op)) + (while (setq ip (car topl) + topl (cdr topl)) + (pbp-make-top-extent ip (car topl))) + (pbp-make-top-extent ip (point-max))))) + +(defun proof-shell-strip-annotations (string) + (let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x ))) + (while (< ip l) + (if (>= (aref string ip) proof-shell-first-special-char) + (if (char-equal (aref string ip) proof-shell-start-char) + (progn (incf ip) + (while (< (aref string ip) proof-shell-first-special-char) + (incf ip)))) + (aset out op (aref string ip)) + (incf op)) + (incf ip)) + (substring out 0 op))) + +(defun proof-shell-handle-error (cmd string) + (save-excursion + (display-buffer (set-buffer proof-pbp-buffer)) + (goto-char (point-max)) + (if (re-search-backward pbp-error-regexp nil t) + (delete-region (- (point) 2) (point-max))) + (newline 2) + (insert-string string) + (beep)) + (set-buffer proof-script-buffer) + (proof-segment-buffer proof-locked-hwm proof-locked-hwm) + (delete-spans (proof-end-of-locked) (point-max) 'type) + (proof-release-lock)) + +(defvar proof-shell-delayed-output nil + "The last interesting output the proof process output, and what to do + with it.") + +(defun proof-shell-handle-delayed-output () + (let ((ins (car proof-shell-delayed-output)) + (str (cdr proof-shell-delayed-output))) + (display-buffer proof-pbp-buffer) + (save-excursion + (cond + ((eq ins 'insert) + (setq str (proof-shell-strip-annotations str)) + (set-buffer proof-pbp-buffer) + (insert str)) + ((eq ins 'analyse) + (proof-shell-analyse-structure str)) + (t (set-buffer proof-pbp-buffer) + (insert "\n\nbug???"))))) + (setq proof-shell-delayed-output (cons 'insert "done"))) + + +(defun proof-shell-process-output (cmd string) + (cond + ((string-match proof-shell-error-regexp string) + (cons 'error (proof-shell-strip-annotations string))) + + ((string-match proof-shell-abort-goal-regexp string) + (setq proof-shell-delayed-output (cons 'insert "\n\nAborted")) + ()) + + ((string-match proof-shell-proof-completed-regexp string) + (setq proof-shell-delayed-output + (cons 'insert (concat "\n" (match-string 0 string))))) + + ((string-match proof-shell-start-goals-regexp string) + (let (start end) + (while (progn (setq start (match-end 0)) + (string-match proof-shell-start-goals-regexp + string start))) + (string-match proof-shell-end-goals-regexp string start) + (setq proof-shell-delayed-output + (cons 'analyse (substring string start end))))) + + ((string-match proof-shell-result-start string) + (let (start end) + (setq start (+ 1 (match-end 0))) + (string-match proof-shell-result-end string) + (setq end (- (match-beginning 0) 1)) + (cons 'loopback (substring string start end)))) + + ((string-match "^Module" cmd) + (setq proof-shell-delayed-output (cons 'insert "Imports done!"))) + + (t (setq proof-shell-delayed-output (cons 'insert string))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Low-level commands for shell communication ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - (erase-buffer) - (funcall proof-shell-mode-is) - (setq comint-prompt-regexp proof-shell-prompt-pattern) - (setq comint-input-sender 'proof-input-sender) - (and running-emacs19 (setq comint-scroll-show-maximum-output t)) - (proof-display-buffer buffer-name) - (set-buffer buffer-name) - ) +(defun proof-shell-insert (string) + (goto-char (point-max)) + (insert (funcall proof-shell-config) string) + (if (not (span-property proof-mark-ext 'detached)) + (set-span-endpoints proof-mark-ext (point) (point))) + (comint-send-input)) + +(defun proof-send (string) + (let ((l (length string)) (i 0)) + (while (< i l) + (if (= (aref string i) ?\n) (aset string i ?\ )) + (incf i))) + (save-excursion + (set-buffer proof-shell-buffer) + (proof-shell-insert string))) + +;; grab the process and return t, otherwise return nil. Note that this +;; is not really intended for anything complicated - just to stop the +;; user accidentally sending a command while the queue is running. + +(defun proof-check-process-available () + (if (proof-shell-live-buffer) + (if proof-shell-busy (error "Proof Process Busy!"))) + (if (not (eq proof-script-buffer (current-buffer))) + (error "Don't own proof process")) + (if (not (eq proof-buffer-type 'script)) + (error "Must be running in a script buffer"))) + +(defun proof-grab-lock () + (proof-start-shell) + (proof-check-process-available) + (setq proof-shell-busy t)) + +(defun proof-release-lock () + (if (proof-shell-live-buffer) + (progn + (if (not proof-shell-busy) + (error "Bug: Proof process not busy")) + (if (not (eq proof-script-buffer (current-buffer))) + (error "Bug: Don't own process")) + (setq proof-shell-busy nil)))) + +; Pass start and end as nil if the cmd isn't in the buffer. + +(defun proof-start-queue (start end alist) + (if start + (if (eq (proof-end-of-locked) start) + (proof-segment-buffer start end) + (proof-segment-buffer end start))) + (while (and alist (string= (cadar alist) "COMMENT")) + (funcall (caddar alist) (caar alist)) + (setq alist (cdr alist))) + (if alist + (progn + (proof-grab-lock) + (erase-buffer proof-pbp-buffer) + (setq proof-shell-delayed-output (cons 'insert "Done.")) + (setq proof-action-list alist) + (proof-send (cadar alist))))) + +; returns t if it's run out of input + +(defun proof-shell-exec-loop () + (save-excursion + (set-buffer proof-script-buffer) + (if (null proof-action-list) (error "Non Sequitur")) + (funcall (caddar proof-action-list) (caar proof-action-list)) + (setq proof-action-list (cdr proof-action-list)) + (while (and proof-action-list + (string= (cadar proof-action-list) "COMMENT")) + (funcall (caddar proof-action-list) (caar proof-action-list)) + (setq proof-action-list (cdr proof-action-list))) + (if (null proof-action-list) + (progn (proof-release-lock) + (proof-segment-buffer proof-locked-hwm proof-locked-hwm) + t) + (proof-send (cadar proof-action-list))))) + +(defun proof-shell-insert-loopback-cmd (cmd) + "Insert command sequence triggered by the proof process +at the end of locked region (after inserting a newline)." + (save-excursion + (set-buffer proof-script-buffer) + (let (ext) + (proof-goto-end-of-locked) + (newline) + (insert cmd) + (setq ext (make-span (proof-end-of-locked) (point))) + (set-span-property ext 'type 'pbp) + (set-span-property ext 'cmd cmd) + (proof-segment-buffer (proof-end-of-locked) (point)) + (setq proof-action-list + (cons (car proof-action-list) + (cons (list ext cmd 'proof-done-advancing) + (cdr proof-action-list))))))) + +(defun proof-shell-popup-eager-annotation () + (let (mrk str file module) + (save-excursion ;; BROKEN - MAY BE MULTI + (goto-char (point-max)) + (search-backward proof-shell-eager-annotation-start) + (setq mrk (+ 1 (point))) + (search-forward proof-shell-eager-annotation-end) + (setq str (buffer-substring mrk (- (point) 1))) + (display-buffer (set-buffer proof-pbp-buffer)) + (insert str "\n")) + (if (string-match "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]" str) + (progn + (setq file (match-string 2 str) + module (match-string 1 str)) + (if (string= file "") + (setq file (buffer-file-name proof-script-buffer))) + (setq file (expand-file-name file)) + (if (string-match "\\(.*\\)\\.." file) + (setq file (match-string 1 file))) + (setq proof-included-files-list (cons (cons module file) + proof-included-files-list)))))) + +(defun proof-shell-filter (str) + (if (string-match proof-shell-eager-annotation-end str) + (proof-shell-popup-eager-annotation)) + (if (string-match (char-to-string proof-shell-wakeup-char) str) + (if (span-property proof-mark-ext 'detached) + (progn + (goto-char (point-min)) + (re-search-forward proof-shell-annotated-prompt-regexp) + (set-span-endpoints proof-mark-ext (point) (point)) + (backward-delete-char 1)) + (let (string mrk res cmd) + (goto-char (setq mrk (span-start proof-mark-ext))) + (re-search-forward proof-shell-annotated-prompt-regexp nil t) + (set-span-endpoints proof-mark-ext (point) (point)) + (backward-char (- (match-end 0) (match-beginning 0))) + (setq string (buffer-substring mrk (point))) + (if proof-shell-sanitise + (progn + (delete-region mrk (point)) + (insert (proof-shell-strip-annotations string)))) + (goto-char (span-start proof-mark-ext)) + (backward-delete-char 1) + (setq cmd (cadar proof-action-list)) + (save-excursion + (setq res (proof-shell-process-output cmd string)) + (cond + ((and (consp res) (eq (car res) 'error)) + (proof-shell-handle-error cmd (cdr res))) + ((and (consp res) (eq (car res) 'loopback)) + (proof-shell-insert-loopback-cmd (cdr res)) + (proof-shell-exec-loop)) + (t (if (proof-shell-exec-loop) + (proof-shell-handle-delayed-output))))))))) + +(defun proof-steal-process () + (proof-start-shell) + (if proof-shell-busy (error "Proof Process Busy!")) + (if (not (eq proof-buffer-type 'script)) + (error "Must be running in a script buffer")) + (cond + ((eq proof-script-buffer (current-buffer)) + nil) + ((or (null proof-script-buffer) (not (buffer-live-p proof-script-buffer))) + (setq proof-script-buffer (current-buffer)) + (proof-init-segmentation) + nil) + (t + (let ((flist proof-included-files-list) + (file (expand-file-name (buffer-file-name))) ext cmd) + (if (string-match "\\(.*\\)\\.." file) (setq file (match-string 1 file))) + (while (and flist (not (string= file (cdar flist)))) + (setq flist (cdr flist))) + (if (null flist) + (if (not (y-or-n-p "Steal script management? " )) (error "Aborted")) + (if (not (y-or-n-p "Reprocess this file? " )) (error "Aborted"))) + (save-excursion + (set-buffer proof-script-buffer) + (setq ext (span-at-before (proof-end-of-locked) 'type)) + (while (and ext (not (memq (span-property ext 'type) + '(goalsave comment))) + (not (string-match "^Goal" (span-property ext 'cmd)))) + (setq ext (prev-span ext 'type))) + (setq cmd (if (and ext (let ((cmd (span-property ext 'cmd))) + (and cmd (string-match "^Goal" cmd)))) + "KillRef; " "")) + (proof-segment-buffer nil nil) + (delete-spans (point-min) (point-max) 'type)) + (setq proof-script-buffer (current-buffer)) + (proof-segment-buffer nil nil) + + (cond + (flist + (list nil (concat cmd "ForgetMark " (caar flist) ";") + `(lambda (ext) (setq proof-included-files-list + (quote ,(cdr flist)))))) + ((not (string= cmd "")) + (list nil cmd 'proof-done-invisible)) + (t nil)))))) -(defun proof-shell-exit () - "Exit the PROOF process +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Script management ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; Script management uses two major segments: Locked, which marks text +; which has been sent to the proof assistant and cannot be altered +; without being retracted, and Queue, which contains stuff being +; queued for processing. proof-action-list contains a list of +; (extent,command,action) triples. The loop looks like: Execute the +; command, and if it's successful, do action on extent. If the +; command's not successful, we bounce the rest of the queue and do +; some error processing. +; +; when an extent has been processed, we classify it as follows: +; 'goalsave - denoting a 'goalsave pair in the locked region +; a 'goalsave region has a 'name property which is the name of the goal +; 'pbp - denoting an extent created by pbp +; 'vanilla - denoting any other extent. +; 'pbp & 'vanilla extents have a property 'cmd, which says what +; command they contain. + +; We don't allow commands while the queue has anything in it. So we +; do configuration by concatenating the config command on the front in +; proof-send + +(defun proof-done-invisible (ext) ()) + +(defun proof-invisible-command (cmd) + (proof-check-process-available) + (if (not (string-match proof-re-end-of-cmd cmd)) + (setq cmd (concat cmd proof-terminal-string))) + (proof-start-queue nil nil (list (list nil cmd 'proof-done-invisible)))) + +(defun proof-insert-pbp-command (cmd) + (proof-check-process-available) + (let (ext) + (proof-goto-end-of-locked) + (insert cmd) + (setq ext (make-span (proof-end-of-locked) (point))) + (set-span-property ext 'type 'pbp) + (set-span-property ext 'cmd cmd) + (proof-start-queue (proof-end-of-locked) (point) + (list (list ext cmd 'proof-done-advancing))))) + +(defun proof-done-advancing (ext) + (let ((end (span-end ext)) nam gext next cmd) + (proof-segment-buffer end proof-queue-loose-end) + (setq cmd (span-property ext 'cmd)) + (cond + ((or (eq (span-property ext 'type) 'comment) + (not (string-match proof-save-command-regexp cmd))) + (set-span-property ext 'highlight 'mouse-face)) + (t + (if (string-match proof-save-with-hole-regexp cmd) + (setq nam (match-string 2 cmd))) + (setq gext ext) + (while (or (eq (span-property gext 'type) 'comment) + (not (string-match proof-goal-command-regexp + (setq cmd (span-property gext 'cmd))))) + (setq next (prev-span gext 'type)) + (delete-span gext) + (setq gext next)) + (if (null nam) + (if (let ((cmd (span-property gext 'cmd))) + (and cmd (string-match proof-goal-with-hole-regexp cmd))) + (setq nam (match-string 1 cmd)) + (error "Oops... can't find Goal name!!!"))) + (set-span-end gext end) + (set-span-property gext 'highlight 'mouse-face) + (set-span-property gext 'type 'goalsave) + (set-span-property gext 'name nam))))) + +; Create a list of (type,int,string) pairs from the end of the locked +; region to pos, denoting the command and the position of its +; terminator. type is one of comment, or cmd. 'unclosed-comment +; may be consed onto the start if the segment finishes with an +; unclosed comment - Runs proof-shell-exit-hook if non nil" +(defun proof-segment-up-to (pos) + (save-excursion + (let ((str (make-string (- (buffer-size) (proof-end-of-locked) -10) ?x)) + (i 0) (depth 0) done alist c) + (proof-goto-end-of-locked) + (while (not done) + (cond + ((and (= (point) pos) (> depth 0)) + (setq done t alist (cons 'unclosed-comment alist))) + ((= (point) (point-max)) + (setq done t)) + ((looking-at "\\*)") + (if (= depth 0) + (progn (message "Warning: extraneous comment end") (setq done t)) + (setq depth (- depth 1)) (forward-char 2) + (if (eq i 0) + (setq alist (cons (list 'comment "" (point)) alist)) + (aset str i ?\ ) (incf i)))) + ((looking-at "(\\*") + (setq depth (+ depth 1)) (forward-char 2)) + ((> depth 0) (forward-char)) + (t + (setq c (char-after (point))) + (if (or (> i 0) (not (= (char-syntax c) ?\ ))) + (progn (aset str i c) (incf i))) + (forward-char) + (if (= c proof-terminal-char) + (progn + (setq alist + (cons (list 'cmd (substring str 0 i) (point)) alist)) + (if (>= (point) pos) (setq done t) (setq i 0))))))) + alist))) + +(defun proof-semis-to-vanillas (semis) + (let ((ct (proof-end-of-locked)) ext alist) + (while (not (null semis)) + (setq ext (make-span ct (caddar semis)) + ct (caddar semis)) + (if (eq (caar semis) 'cmd) + (progn + (set-span-property ext 'type 'vanilla) + (set-span-property ext 'cmd (cadar semis)) + (setq alist (cons (list ext (cadar semis) 'proof-done-advancing) + alist))) + (set-span-property ext 'type 'comment) + (setq alist (cons (list ext "COMMENT" 'proof-done-advancing) alist))) + (setq semis (cdr semis))) + (nreverse alist))) + +(defun proof-assert-until-point () + (interactive) + (let ((pt (point)) semis crowbar vanillas) + (setq crowbar (proof-steal-process)) + (save-excursion + (if (not (re-search-backward "\\S-" (proof-end-of-locked) t)) + (progn (goto-char pt) + (error "Nothing to do!"))) + (setq semis (proof-segment-up-to (point))) + (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis))) + (if (and (not crowbar) (null semis)) (error "Nothing to do!"))) + (goto-char (caddar semis)) + (setq vanillas (proof-semis-to-vanillas (nreverse semis))) + (if crowbar (setq vanillas (cons crowbar vanillas))) + (proof-start-queue (proof-end-of-locked) (point) vanillas))) + +(defun proof-done-retracting (ext &optional delete-region) + "Updates display after proof process has reset its state. See also +the documentation for `proof-retract-until-point'. It optionally +deletes the region corresponding to the proof sequence." + (let ((start (span-start ext)) + (end (span-end ext))) + (proof-segment-buffer start proof-queue-loose-end) + (delete-spans start end 'type) + (delete-span ext) + (if delete-region (delete-region start end)))) + + +(defun proof-retract-setup-actions (start end proof-command delete-region) + (list (list (make-span start end) + proof-command + `(lambda (ext) (proof-done-retracting ext ,delete-region))))) + +(defun proof-retract-until-point (&optional delete-region) + "Sets up the proof process for retracting until point. In + particular, it sets a flag for the filter process to call + `proof-done-retracting' after the proof process has actually + successfully reset its state. It optionally deletes the region in + the proof script corresponding to the proof command sequence." + (interactive) + (proof-check-process-available) + (let ((sext (span-at (point) 'type)) + (end (proof-end-of-locked)) + ext start actions) + (if (null end) (error "No locked region")) + (if (or (null sext) (< end (point))) (error "Outside locked region")) + + (setq start (span-start sext)) + (setq ext (span-at-before end 'type)) + (while (let ((cmd (span-property ext 'cmd))) + (and ext cmd + (not (string-match proof-goal-command-regexp cmd)) + (not (eq (span-property ext 'type) 'goalsave)))) + (setq ext (prev-span ext 'type))) + + (if (let ((cmd (span-property ext 'cmd))) + (and ext cmd (string-match proof-goal-command-regexp cmd))) + (if (<= (span-end ext) (point)) + (progn + (setq ext sext) + (while (and ext (eq (span-property ext 'type) 'comment)) + (setq ext (next-span ext 'type))) + (setq actions (proof-retract-setup-actions + start end + (if (null ext) "COMMENT" + (funcall proof-undo-target-fn ext)) + delete-region) + end start)) + + (setq actions (proof-retract-setup-actions (span-start ext) end + proof-kill-goal-command + delete-region) + end (span-start ext)))) + + (if (> end start) + (setq actions + (nconc (proof-retract-setup-actions + start end + (funcall proof-forget-target-fn sext) + delete-region) + actions))) + (proof-start-queue (min start end) (proof-end-of-locked) actions))) + +(defun proof-undo-last-successful-command () + "Undo last successful command, both in the buffer recording the + proof script and in the proof process. In particular, it deletes + the corresponding part of the proof script." + (interactive) + (goto-char (span-start (span-at-before (proof-end-of-locked) 'type))) + (proof-retract-until-point t)) +(defun proof-restart-script () (interactive) (save-excursion - (let ((buffer (proof-shell-buffer))) - (and buffer - (progn - (save-excursion - (set-buffer buffer) - (comint-send-eof)) - (kill-buffer buffer) - - (run-hooks 'proof-shell-exit-hook) - - ;;it is important that the hooks are - ;;run after the buffer has been killed. In the reverse - ;;order e.g., intall-shell-fonts causes problems and it - ;;is impossilbe to restart the PROOF shell - - (message - (format "%s process terminated." proof-shell-process-name))))))) - + (set-buffer proof-script-buffer) + (delete-spans (point-min) (point-max) 'type) + (proof-segment-buffer nil nil) + (setq proof-shell-busy nil + proof-script-buffer nil) + (if (get-buffer proof-shell-buffer) + (kill-buffer proof-shell-buffer)) + (if (get-buffer proof-pbp-buffer) + (kill-buffer proof-pbp-buffer)))) + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Active terminator minor mode ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defvar proof-active-terminator-minor-mode nil) +(defvar proof-active-terminator-minor-mode nil +"active terminator minor mode flag") + (make-variable-buffer-local 'proof-active-terminator-minor-mode) (put 'proof-active-terminator-minor-mode 'permanent-local t) @@ -417,77 +1132,39 @@ current command." (or (assq 'proof-active-terminator-minor-mode minor-mode-alist) (setq minor-mode-alist (append minor-mode-alist - (list '(proof-active-terminator-minor-mode " ;"))))) + (list '(proof-active-terminator-minor-mode + (concat " " proof-terminal-string)))))) (setq proof-active-terminator-minor-mode (if (null arg) (not proof-active-terminator-minor-mode) (> (prefix-numeric-value arg) 0))) - (if (fboundp 'redraw-modeline) (redraw-modeline) (force-mode-line-update))) + (if (fboundp 'redraw-modeline) (redraw-modeline) (redraw-modeline))) (defun proof-active-terminator () (interactive) (if proof-active-terminator-minor-mode (proof-process-active-terminator) (self-insert-command 1))) - -(defun proof-process-active-terminator () - "Process an active terminator key-press" - - (interactive) - (let (start) - (and (re-search-backward "[^ ]" nil t) - (not (char-equal (following-char) proof-terminal-char)) - (forward-char)) - (save-excursion - (setq start (proof-find-start-of-command))) - (if (not start) - (self-insert-command 1) - (if (> start (point)) - (setq start (point))) - (proof-simulate-send-region start (point) t) - (if (char-equal proof-terminal-char (following-char)) - (forward-char) - (self-insert-command 1))))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; font lock faces: declarations, errors, tacticals ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defun proof-process-active-terminator () + "Insert the terminator in an intelligent way and send the commands + between the previous and the new terminator to the proof process." + (proof-check-process-available) + (let ((mrk (point)) ins semis) + (if (looking-at "\\s-\\|\\'\\|\\w") + (if (not (re-search-backward "\\S-" (proof-end-of-locked) t)) + (error "Nothing to do!"))) + (if (not (= (char-after (point)) proof-terminal-char)) + (progn (forward-char) (insert proof-terminal-string) (setq ins t))) + (setq semis (proof-segment-up-to (point))) + (if (null semis) (error "Nothing to do!")) + (if (eq 'unclosed-comment (car semis)) + (progn (if ins (backward-delete-char 1)) + (goto-char mrk) (insert proof-terminal-string)) + (goto-char (caddar (last semis))) + (proof-start-queue (proof-end-of-locked) (point) + (proof-semis-to-vanillas semis))))) -(defvar font-lock-declaration-name-face -(progn - (cond ((x-display-color-p) - ;notice that device-class does not exist in Emacs 19.30 - - (copy-face 'bold 'font-lock-declaration-name-face) - - ;; Emacs 19.28 compiles this down to - ;; internal-set-face-1. This is not compatible with XEmacs - (dont-compile - (set-face-foreground - 'font-lock-declaration-name-face "chocolate"))) - (t (copy-face 'bold-italic 'font-lock-declaration-name-face))) - (if running-emacs19 - (setq font-lock-declaration-name-face - (face-name 'font-lock-declaration-name-face))))) - -(defvar font-lock-tacticals-name-face -(if (x-display-color-p) - (let ((face (make-face 'font-lock-tacticals-name-face))) - (dont-compile - (set-face-foreground face - "MediumOrchid3")) - face) - (copy-face 'bold 'font-lock-tacticals-name-face))) - -(defvar font-lock-error-face -(if (x-display-color-p) - (let ((face (make-face 'font-lock-error-face))) - (dont-compile - (set-face-foreground face - "red")) - face) - (copy-face 'bold 'font-lock-error-face))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -499,17 +1176,7 @@ current command." (define-derived-mode proof-mode fundamental-mode "Proof" "Proof mode - not standalone" - ()) - -(define-key proof-mode-map [(control c) (control e)] - 'proof-find-end-of-command) -(define-key proof-mode-map [(control c) (control j)] 'proof-send-line) -(define-key proof-mode-map [(control c) (control r)] 'proof-send-region) -(define-key proof-mode-map [(control c) (control c)] 'proof-interrupt-subjob) - -(define-derived-mode proof-shell-mode comint-mode - "proof-shell" "Proof shell mode - not standalone" - ()) + (setq proof-buffer-type 'script)) ;; the following callback is an irritating hack - there should be some ;; elegant mechanism for computing constants after the child has @@ -534,13 +1201,59 @@ current command." (concat proof-terminal-string "\\|" (regexp-quote proof-comment-start) "\\|" (regexp-quote proof-comment-end))) + +;; keymap + (define-key proof-mode-map (vconcat [(control c)] (vector proof-terminal-char)) 'proof-active-terminator-minor-mode) (define-key proof-mode-map proof-terminal-char 'proof-active-terminator) + (define-key proof-mode-map [(control c) (control a)] 'proof-assert-until-point) + (define-key proof-mode-map [(control c) u] 'proof-retract-until-point) + (define-key proof-mode-map [(control c) (control u)] 'proof-undo-last-successful-command) + (define-key proof-mode-map [(control c) ?'] + 'proof-goto-end-of-locked) - ) + ;; For fontlock + (remove-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer t) + (add-hook 'font-lock-after-fontify-buffer-hook 'proof-zap-commas-buffer nil t) + (remove-hook 'font-lock-mode-hook 'proof-unfontify-separator t) + (add-hook 'font-lock-mode-hook 'proof-unfontify-separator nil t) +;; if we don't have the following, zap-commas fails to work. + + (setq font-lock-always-fontify-immediately t)) + +(define-derived-mode proof-shell-mode comint-mode + "proof-shell" "Proof shell mode - not standalone" + (setq proof-buffer-type 'shell) + (setq proof-shell-busy nil) + (setq proof-shell-delayed-output (cons 'insert "done")) + (setq comint-prompt-regexp proof-shell-prompt-pattern) + (add-hook 'comint-output-filter-functions 'proof-shell-filter nil t) +; (add-hook 'comint-output-filter-functions 'comint-truncate-buffer nil t) +; (setq comint-buffer-maximum-size 10000) + (setq comint-append-old-input nil) + (setq proof-mark-ext (make-extent nil nil (current-buffer))) + (set-span-property proof-mark-ext 'detachable nil) + (set-span-property proof-mark-ext 'start-closed t) + (set-span-property proof-mark-ext 'end-open t)) + +(defun proof-shell-config-done () + (accept-process-output (get-buffer-process (current-buffer))) + (if proof-shell-init-cmd + (proof-shell-insert proof-shell-init-cmd)) + (while (span-property proof-mark-ext 'detached) + (if (accept-process-output (get-buffer-process (current-buffer)) 5) + () + (error "Failed to initialise proof process")))) + +(define-derived-mode pbp-mode fundamental-mode + (setq proof-buffer-type 'pbp) + "Proof" "Proof by Pointing" + ;; defined-derived-mode pbp-mode initialises pbp-mode-map + (suppress-keymap pbp-mode-map) + (erase-buffer)) (provide 'proof) |