diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pbp.el | 2 | ||||
| -rw-r--r-- | generic/proof-indent.el | 124 | ||||
| -rw-r--r-- | generic/proof-syntax.el | 104 | ||||
| -rw-r--r-- | generic/proof.el | 1838 | ||||
| -rw-r--r-- | generic/span-extent.el | 82 | ||||
| -rw-r--r-- | generic/span-overlay.el | 291 |
6 files changed, 2441 insertions, 0 deletions
diff --git a/generic/pbp.el b/generic/pbp.el new file mode 100644 index 00000000..23ffdd68 --- /dev/null +++ b/generic/pbp.el @@ -0,0 +1,2 @@ + +(provide 'pbp) diff --git a/generic/proof-indent.el b/generic/proof-indent.el new file mode 100644 index 00000000..bb42f462 --- /dev/null +++ b/generic/proof-indent.el @@ -0,0 +1,124 @@ +;; proof-indent.el Generic Indentation for Proof Assistants +;; Copyright (C) 1997, 1998 LFCS Edinburgh +;; Authors: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> + +(require 'cl) +(require 'proof-syntax) + +(defvar proof-stack-to-indent nil + "Prover-specific code for indentation.") + +(defvar proof-parse-indent nil + "Proof-assistant specific function for parsing characters for + indentation which is invoked in `proof-parse-to-point.'. Must be a + function taking two arguments, a character (the current character) + and a stack reflecting indentation, and must return a stack. The + stack is a list of the form (c . p) where `c' is a character + representing the type of indentation and `p' records the column for + indentation. The generic `proof-parse-to-point.' function supports + parentheses and commands. It represents these with the characters + `?\(', `?\[' and `proof-terminal-char'. ") + +;; This is quite different from sml-mode, but borrows some bits of +;; code. It's quite a lot less general, but works with nested +;; comments. + +;; parse-to-point: If from is nil, parsing starts from either +;; proof-locked-end if we're in the proof-script-buffer or the +;; beginning of the buffer. Otherwise state must contain a valid +;; triple. + +(defun proof-parse-to-point (&optional from state) + (let ((comment-level 0) (stack (list (list nil 0))) + (end (point)) instring c) + (save-excursion + (if (null from) + (if (eq proof-script-buffer (current-buffer)) + (proof-goto-end-of-locked) + (goto-char 1)) + (goto-char from) + (setq instring (car state) + comment-level (nth 1 state) + stack (nth 2 state))) + (while (< (point) end) + (setq c (char-after (point))) + (cond + (instring + (if (eq c ?\") (setq instring nil))) + (t (cond + ((eq c ?\() + (cond + ((looking-at "(\\*") + (progn + (incf comment-level) + (forward-char))) + ((eq comment-level 0) + (setq stack (cons (list ?\( (point)) stack))))) + ((and (eq c ?\*) (looking-at "\\*)")) + (decf comment-level) + (forward-char)) + ((> comment-level 0)) + ((eq c ?\") (setq instring t)) + ((eq c ?\[) + (setq stack (cons (list ?\[ (point)) stack))) + ((or (eq c ?\)) (eq c ?\])) + (setq stack (cdr stack))) + ((looking-at proof-commands-regexp) + (setq stack (cons (list proof-terminal-char (point)) stack))) + ((and (eq c proof-terminal-char) + (eq (car (car stack)) proof-terminal-char)) (cdr stack)) + (proof-parse-indent + (setq stack (funcall proof-parse-indent c stack)))))) + (forward-char)) + (list instring comment-level stack)))) + +(defun proof-indent-line () + (interactive) + (if (and (eq proof-script-buffer (current-buffer)) + (< (point) (proof-locked-end))) + (if (< (current-column) (current-indentation)) + (skip-chars-forward "\t ")) + (save-excursion + (beginning-of-line) + (let* ((state (proof-parse-to-point)) + (beg (point)) + (indent (cond ((car state) 1) + ((> (nth 1 state) 0) 1) + (t (funcall proof-stack-to-indent (nth 2 state)))))) + (skip-chars-forward "\t ") + (if (not (eq (current-indentation) indent)) + (progn (delete-region beg (point)) + (indent-to indent))))) + (skip-chars-forward "\t "))) + +(defun proof-indent-region (start end) + (interactive "r") + (if (and (eq proof-script-buffer (current-buffer)) + (< (point) (proof-locked-end))) + (error "can't indent locked region!")) + (save-excursion + (goto-char start) + (beginning-of-line) + (let* ((beg (point)) + (state (proof-parse-to-point)) + indent) + ;; End of region changes with new indentation + (while (< (point) end) + (setq indent + (cond ((car state) 1) + ((> (nth 1 state) 0) 1) + (t (funcall proof-stack-to-indent (nth 2 state))))) + (skip-chars-forward "\t ") + (let ((diff (- (current-indentation) indent))) + (if (not (eq diff 0)) + (progn + (delete-region beg (point)) + (indent-to indent) + (setq end (- end diff))))) + (end-of-line) + (if (< (point) (point-max)) (forward-char)) + (setq state (proof-parse-to-point beg state) + beg (point)))))) + +(provide 'proof-indent)
\ No newline at end of file diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el new file mode 100644 index 00000000..5caa8fe3 --- /dev/null +++ b/generic/proof-syntax.el @@ -0,0 +1,104 @@ +;; proof-syntax.el Generic font lock expressions +;; Copyright (C) 1997-1998 LFCS Edinburgh. +;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequiera +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> + +(require 'font-lock) + +;;; FIXME: change this to proof- +(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 "\\|")) + +;; Generic font-lock + +;; proof-commands-regexp is used for indentation +(defvar proof-commands-regexp "" + "Subset of keywords and tacticals which are terminated by the + `proof-terminal-char'") + + +(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)" + "A regular expression for parsing identifiers.") + +;; For font-lock, we treat ,-separated identifiers as one identifier +;; and refontify commata using \{proof-unfontify-separator}. + +(defun proof-ids (proof-id) + "Function to generate a regular expression for separated lists of + identifiers." + (concat proof-id "\\(\\s-*,\\s-*" proof-id "\\)*")) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; font lock faces: declarations, errors, tacticals ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-have-color () + ()) + +(defvar font-lock-declaration-name-face +(progn + (cond + ((proof-have-color) + (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 + (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 (proof-have-color) + (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 (proof-have-color) + (let ((face (make-face 'font-lock-error-face))) + (dont-compile + (set-face-foreground face "red")) + face) + (copy-face 'bold 'font-lock-error-face))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; A big hack to unfontify commas in declarations and definitions. ;; +;; All that can be said for it is that the previous way of doing ;; +;; this was even more bogus. ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Refontify the whole line, 'cos that's what font-lock-after-change +;; does. + +(defun proof-zap-commas-region (start end length) + (save-excursion + (let + ((start (progn (goto-char start) (beginning-of-line) (point))) + (end (progn (goto-char end) (end-of-line) (point)))) + (goto-char start) + (while (search-forward "," end t) + (if (memq (get-char-property (- (point) 1) 'face) + '(font-lock-declaration-name-face + font-lock-function-name-face)) + (font-lock-remove-face (- (point) 1) (point)) + ))))) + +(defun proof-zap-commas-buffer () + (proof-zap-commas-region (point-min) (point-max) 0)) + +(defun proof-unfontify-separator () + (make-local-variable 'after-change-functions) + (setq after-change-functions + (append (delq 'proof-zap-commas-region after-change-functions) + '(proof-zap-commas-region)))) + + +(provide 'proof-syntax) diff --git a/generic/proof.el b/generic/proof.el new file mode 100644 index 00000000..c37f863b --- /dev/null +++ b/generic/proof.el @@ -0,0 +1,1838 @@ +;; proof.el Major mode for proof assistants +;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, +;; Thomas Kleymann and Dilip Sequeira + +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> +;; Thanks to Robert Boyer, Rod Burstall, +;; James McKinna, Mark Ruys, Martin Steffen, Perdita Stevens + + +(require 'cl) +(require 'compile) +(require 'comint) +(require 'etags) +(cond ((fboundp 'make-extent) (require 'span-extent)) + ((fboundp 'make-overlay) (require 'span-overlay)) + (t nil)) +(require 'proof-syntax) +(require 'proof-indent) +(require 'easymenu) +(require 'tl-list) + +(autoload 'w3-fetch "w3" nil t) + +(defmacro deflocal (var value docstring) + (list 'progn + (list 'defvar var 'nil docstring) + (list 'make-variable-buffer-local (list 'quote var)) + (list 'setq var value))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Generic config for proof assistant ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-assistant "" + "Name of the proof assistant") + +(defvar proof-www-home-page "" + "Web address for information on proof assistant") + +(defvar proof-shell-cd nil + "*Command of the inferior process to change the directory.") + +(defvar proof-shell-process-output-system-specific nil + "*Errors, start of proofs, abortions of proofs and completions of + proofs are recognised in the function `proof-shell-process-output'. + All other output from the proof engine is simply reported to the + user in the RESPONSE buffer. + + To catch further special cases, set this variable to a tuple of + functions '(condf . actf). Both are given (cmd string) as arguments. + `cmd' is a string containing the currently processed command. + `string' is the response from the proof system. To change the + behaviour of `proof-shell-process-output', (condf cmd string) must + return a non-nil value. Then (actf cmd string) is invoked. See the + documentation of `proof-shell-process-output' for the required + output format.") + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proof mode variables ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defconst proof-mode-version-string + "PROOF-MODE. ALPHA Version 2 (August 1998) LEGO Team <lego@dcs.ed.ac.uk>") + +(defconst proof-info-dir "/usr/local/share/info" + "Directory to search for Info documents on Script Management.") + +(defconst proof-universal-keys + (list (cons '[(control c) (control c)] 'proof-interrupt-process) + (cons '[(control c) (control v)] + 'proof-execute-minibuffer-cmd) + (cons '[(meta tab)] 'tag-complete-symbol)) + "List of keybindings which are valid in both in the script and the + response buffer. Elements of the list are tuples (k . f) + where `k' is a keybinding (vector) and `f' the designated function.") + +(defvar proof-prog-name-ask-p nil + "*If t, you will be asked which program to run when the inferior + process starts up.") + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Other buffer-local variables used by proof mode ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; These should be set before proof-config-done is called + +(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-with-hole-regexp nil "Matches a saved goal command") + +(defvar proof-goal-command-p nil "Is this a goal") +(defvar proof-count-undos-fn nil "Compute number of undos in a target segment") +(defvar proof-find-and-forget-fn nil "Compute command to forget up to point") + +(defvar proof-goal-hyp-fn nil + "A function which returns cons cell if point is at a goal/hypothesis. +First element of cell is a symbol, 'goal' or 'hyp'. The second +element is a string: the goal or hypothesis itself. This is used +when parsing the proofstate output") + +(defvar proof-kill-goal-command nil "How to kill a goal.") +(defvar proof-global-p nil + "Is this a global declaration") + +(defvar proof-state-preserving-p nil + "A predicate, non-nil if its argument preserves the proof state") + +(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-insert-hook nil + "Function to config proof-system to interface") + +(defvar proof-pre-shell-start-hook) +(defvar proof-post-shell-exit-hook) + +(defvar proof-shell-prompt-pattern nil + "comint-prompt-pattern for proof shell") + +(defvar proof-shell-init-cmd nil + "The command for initially configuring the proof process") + +(defvar proof-shell-handle-delayed-output-hook + '(proof-pbp-focus-on-first-goal) + "*This hook is called after output from the PROOF process has been + displayed in the RESPONSE buffer.") + +(defvar proof-shell-handle-error-hook + '(proof-goto-end-of-locked-if-pos-not-visible-in-window) + "*This hook is called after an error has been reported in the + RESPONSE buffer.") + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Generic config for script management ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-shell-wakeup-char nil + "A character terminating the prompt in annotation mode") + +(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.") + +(defvar proof-shell-error-regexp nil + "A regular expression indicating that the PROOF process has + identified an error.") + +(defvar proof-shell-interrupt-regexp nil + "A regular expression indicating that the PROOF process has + responded to an interrupt.") + +(defvar proof-shell-proof-completed-regexp nil + "*Regular expression indicating that the proof has been completed.") + +(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.") + +(defvar proof-shell-end-goals-regexp "" + "String indicating the end of the proof state.") + +(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-mode-name "Proof") + +(defvar proof-shell-echo-input t + "If nil, input to the proof shell will not be echoed") + +(defvar proof-terminal-string nil + "End-of-line string for proof process.") + +(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-marker 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") + +(deflocal proof-active-buffer-fake-minor-mode nil + "An indication in the modeline that this is the *active* buffer") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; A couple of small utilities ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-define-keys (map kbl) + "Adds keybindings `kbl' in `map'. The argument `kbl' is a list of + tuples (k . f) where `k' is a keybinding (vector) and `f' the + designated function." + (mapcar + (lambda (kbl) + (let ((k (car kbl)) (f (cdr kbl))) + (define-key map k f))) + kbl)) + +(defun proof-string-to-list (s separator) + "converts strings `s' separated by the character `separator' to a + list of words" + (let ((end-of-word-occurence (string-match (concat separator "+") s))) + (if (not end-of-word-occurence) + (if (string= s "") + nil + (list s)) + (cons (substring s 0 end-of-word-occurence) + (proof-string-to-list + (substring s + (string-match (concat "[^" separator "]") + s end-of-word-occurence)) separator))))) + +;; FIXME: this doesn't belong here (and shouldn't be called w3-* !!) +(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))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Basic code for the locked region and the queue region ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defvar proof-locked-hwm nil + "Upper limit of the locked region") + +(defvar proof-queue-loose-end nil + "Limit of the queue region that is not equal to proof-locked-hwm.") + +(defvar proof-locked-span nil + "Upper limit of the locked region") + +(defvar proof-queue-span nil + "Upper limit of the locked region") + +(make-variable-buffer-local 'proof-locked-span) +(make-variable-buffer-local 'proof-queue-span) + +(defun proof-init-segmentation () + (setq proof-queue-loose-end nil) + (if (not proof-queue-span) + (setq proof-queue-span (make-span 1 1))) + (set-span-property proof-queue-span 'start-closed t) + (set-span-property proof-queue-span 'end-open t) + (span-read-only proof-queue-span) + + (make-face 'proof-queue-face) + ;; Whether display has color or not + (cond ((and (fboundp 'device-class) + (eq (device-class (frame-device)) 'color)) + (set-face-background 'proof-queue-face "mistyrose")) + ((and (fboundp 'x-display-color-p) (x-display-color-p)) + (set-face-background 'proof-queue-face "mistyrose")) + (t (progn + (set-face-background 'proof-queue-face "Black") + (set-face-foreground 'proof-queue-face "White")))) + (set-span-property proof-queue-span 'face 'proof-queue-face) + + (detach-span proof-queue-span) + + (setq proof-locked-hwm nil) + (if (not proof-locked-span) + (setq proof-locked-span (make-span 1 1))) + (set-span-property proof-locked-span 'start-closed t) + (set-span-property proof-locked-span 'end-open t) + (span-read-only proof-locked-span) + + (make-face 'proof-locked-face) + ;; Whether display has color or not + (cond ((and (fboundp 'device-class) + (eq (device-class (frame-device)) 'color)) + (set-face-background 'proof-locked-face "lavender")) + ((and (fboundp 'x-display-color-p) (x-display-color-p)) + (set-face-background 'proof-locked-face "lavender")) + (t (set-face-property 'proof-locked-face 'underline t))) + (set-span-property proof-locked-span 'face 'proof-locked-face) + + (detach-span proof-locked-span)) + +(defsubst proof-lock-unlocked () + (span-read-only proof-locked-span)) + +(defsubst proof-unlock-locked () + (span-read-write proof-locked-span)) + +(defsubst proof-set-queue-endpoints (start end) + (set-span-endpoints proof-queue-span start end)) + +(defsubst proof-set-locked-endpoints (start end) + (set-span-endpoints proof-locked-span start end)) + +(defsubst proof-detach-queue () + (and proof-queue-span (detach-span proof-queue-span))) + +(defsubst proof-detach-locked () + (and proof-locked-span (detach-span proof-locked-span))) + +(defsubst proof-set-queue-start (start) + (set-span-endpoints proof-queue-span start (span-end proof-queue-span))) + +(defsubst proof-set-queue-end (end) + (set-span-endpoints proof-queue-span (span-start proof-queue-span) end)) + +(defun proof-detach-segments () + (proof-detach-queue) + (proof-detach-locked)) + +(defsubst proof-set-locked-end (end) + (if (>= (point-min) end) + (proof-detach-locked) + (set-span-endpoints proof-locked-span (point-min) end))) + +(defun proof-unprocessed-begin () + "proof-unprocessed-begin returns end of locked region in script + buffer and point-min otherwise." + (or + (and (eq proof-script-buffer (current-buffer)) + proof-locked-span (span-end proof-locked-span)) + (point-min))) + +(defun proof-locked-end () + "proof-locked-end returns the end of the locked region. It should + only be called if we're in the scripting buffer." + (if (eq proof-script-buffer (current-buffer)) + (proof-unprocessed-begin) + (error "bug: proof-locked-end called from wrong buffer"))) + +(defsubst proof-end-of-queue () + (and proof-queue-span (span-end proof-queue-span))) + +(defun proof-dont-show-annotations () + "This sets the display values of the annotations used to + communicate with the proof assistant so that they don't show up on + the screen." + (let ((disp (make-display-table)) + (i 128)) + (while (< i 256) + (aset disp i []) + (incf i)) + (cond ((fboundp 'add-spec-to-specifier) + (add-spec-to-specifier current-display-table disp + (current-buffer))) + ((boundp 'buffer-display-table) + (setq buffer-display-table disp))))) + +;;; in case Emacs is not aware of read-shell-command-map + +(defvar read-shell-command-map + (let ((map (make-sparse-keymap))) + (if (not (fboundp 'set-keymap-parents)) + (setq map (append minibuffer-local-map map)) + (set-keymap-parents map minibuffer-local-map) + (set-keymap-name map 'read-shell-command-map)) + (define-key map "\t" 'comint-dynamic-complete) + (define-key map "\M-\t" 'comint-dynamic-complete) + (define-key map "\M-?" 'comint-dynamic-list-completions) + map) + "Minibuffer keymap used by shell-command and related commands.") + + +;;; in case Emacs is not aware of the function read-shell-command +(or (fboundp 'read-shell-command) + ;; from minibuf.el distributed with XEmacs 19.11 + (defun read-shell-command (prompt &optional initial-input history) + "Just like read-string, but uses read-shell-command-map: +\\{read-shell-command-map}" + (let ((minibuffer-completion-table nil)) + (read-from-minibuffer prompt initial-input read-shell-command-map + nil (or history + 'shell-command-history))))) + +;; The package fume-func provides a function with the same name and +;; specification. However, fume-func's version is incorrect. +(and (fboundp 'fume-match-find-next-function-name) +(defun fume-match-find-next-function-name (buffer) + "General next function name in BUFFER finder using match. + The regexp is assumed to be a two item list the car of which is the regexp + to use, and the cdr of which is the match position of the function name" + (set-buffer buffer) + (let ((r (car fume-function-name-regexp)) + (p (cdr fume-function-name-regexp))) + (and (re-search-forward r nil t) + (cons (buffer-substring (setq p (match-beginning p)) (point)) p))))) + +(defun proof-goto-end-of-locked-interactive () + "Jump to the end of the locked region." + (interactive) + (switch-to-buffer proof-script-buffer) + (goto-char (proof-locked-end))) + +(defun proof-goto-end-of-locked () + "Jump to the end of the locked region." + (goto-char (proof-locked-end))) + +(defun proof-goto-end-of-locked-if-pos-not-visible-in-window () + "If the end of the locked region is not visible, jump to the end of + the locked region." + (interactive) + (let ((pos (save-excursion + (set-buffer proof-script-buffer) + (proof-locked-end)))) + (or (pos-visible-in-window-p pos (get-buffer-window + proof-script-buffer t)) + (proof-goto-end-of-locked-interactive)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Starting and stopping the proof-system shell ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-shell-live-buffer () + (and proof-shell-buffer + (comint-check-proc proof-shell-buffer) + proof-shell-buffer)) + +(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 + (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)) + + ;; Starting the inferior process (asynchronous) + (let ((prog-name-list (proof-string-to-list proof-prog-name " "))) + (apply 'make-comint (append (list proc (car prog-name-list) nil) + (cdr prog-name-list)))) + ;; To send any initialisation commands to the inferior process, + ;; consult proof-shell-config-done... + + (setq proof-shell-buffer (get-buffer (concat "*" proc "*"))) + (setq proof-pbp-buffer (get-buffer-create (concat "*" proc "-goals*"))) + + (save-excursion + (set-buffer proof-shell-buffer) + (funcall proof-mode-for-shell) + (set-buffer proof-pbp-buffer) + (funcall proof-mode-for-pbp)) + + (setq proof-script-buffer (current-buffer)) + (proof-init-segmentation) + (setq proof-active-buffer-fake-minor-mode t) + + (if (fboundp 'redraw-modeline) + (redraw-modeline) + (force-mode-line-update)) + + (or (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist) + (setq minor-mode-alist + (append minor-mode-alist + (list '(proof-active-buffer-fake-minor-mode + " Scripting"))))) + + (message + (format "Starting %s process... done." proc))))) + + +(defun proof-stop-shell () + "Exit the PROOF process + + Runs proof-shell-exit-hook if non nil" + + (interactive) + (save-excursion + (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-detach-segments)) + (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 + + (message (format "%s process terminated." proc))))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proof by pointing ;; +;; All very lego-specific at present ;; +;; To make sense of this code, you should read the ;; +;; relevant LFCS tech report by tms, yb, and djs ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(defvar pbp-goal-command nil + "Command informing the prover that `pbp-button-action' has been + requested on a goal.") + +(defvar pbp-hyp-command nil + "Command informing the prover that `pbp-button-action' has been + requested on an assumption.") + +(defun pbp-button-action (event) + (interactive "e") + (mouse-set-point event) + (pbp-construct-command)) + +; Using the spans in a mouse behavior is quite simple: from the +; mouse position, find the relevant span, then get its annotation +; and produce a piece of text that will be inserted in the right +; buffer. + +(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 proof-send-span (event) + (interactive "e") + (let* ((span (span-at (mouse-set-point event) 'type)) + (str (span-property span 'cmd))) + (cond ((and (eq proof-script-buffer (current-buffer)) (not (null span))) + (proof-goto-end-of-locked) + (cond ((eq (span-property span 'type) 'vanilla) + (insert str))))))) + +(defun pbp-construct-command () + (let* ((span (span-at (point) 'proof)) + (top-span (span-at (point) 'proof-top-element)) + top-info) + (if (null top-span) () + (setq top-info (span-property top-span 'proof-top-element)) + (pop-to-buffer proof-script-buffer) + (cond + (span + (proof-invisible-command + (format (if (eq 'hyp (car top-info)) pbp-hyp-command + pbp-goal-command) + (concat (cdr top-info) (proof-expand-path + (span-property span 'proof)))))) + ((eq (car top-info) 'hyp) + (proof-invisible-command (format pbp-hyp-command (cdr top-info)))) + (t + (proof-insert-pbp-command (format pbp-change-goal (cdr top-info)))))) + )) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Turning annotated output into pbp goal set ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(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.") + +;; FIXME: da: where is this variable used? +;; dropped in favour of goal-char? +(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-span (start end) + (let (span name) + (goto-char start) + ;; FIXME: why name? This is a character function + (setq name (funcall proof-goal-hyp-fn)) + (beginning-of-line) + (setq start (point)) + (goto-char end) + (beginning-of-line) + (backward-char) + (setq span (make-span start (point))) + (set-span-property span 'mouse-face 'highlight) + (set-span-property span 'proof-top-element name))) + + +;; Need this for processing error strings and so forth + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; The filter. First some functions that handle those few ;; +;; occasions when the glorious illusion that is script-management ;; +;; is temporarily suspended ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Output from the proof process is handled lazily, so that only +;; the output from the last of multiple commands is actually +;; processed (assuming they're all successful) + +(defvar proof-shell-delayed-output nil + "The last interesting output the proof process output, and what to do + with it.") + +(defvar proof-analyse-using-stack nil + "Are annotations sent by proof assistant local or global") + +;; FIXME: da: what's magical value 128 below? should be in defconst? +(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 span) + (while (< ip l) + (if (< (setq c (aref string ip)) 128) + (progn (aset out op c) + (incf op))) + (incf ip)) + (display-buffer (set-buffer proof-pbp-buffer)) + (erase-buffer) + (insert (substring out 0 op)) + + (setq ip 0 + op 1) + (while (< ip l) + (setq c (aref string ip)) + (cond + ((= c proof-shell-goal-char) + (setq topl (cons op topl)) + (setq ap 0)) + ((= c proof-shell-start-char) + (if proof-analyse-using-stack + (setq ap (- ap (- (aref string (incf ip)) 128))) + (setq ap (- (aref string (incf ip)) 128))) + (incf ip) + (while (not (= (setq c (aref string ip)) proof-shell-end-char)) + (aset ann ap (- c 128)) + (incf ap) + (incf ip)) + (setq stack (cons op (cons (substring ann 0 ap) stack)))) + ((= c proof-shell-field-char) + (setq span (make-span (car stack) op)) + (set-span-property span 'mouse-face 'highlight) + (set-span-property span 'proof (car (cdr stack))) + ;; Pop annotation off stack + (and proof-analyse-using-stack + (progn + (setq ap 0) + (while (< ap (length (cadr stack))) + (aset ann ap (aref (cadr stack) ap)) + (incf ap)))) + ;; Finish popping annotations + (setq stack (cdr (cdr stack)))) + (t (incf op))) + (incf ip)) + (setq topl (reverse (cons (point-max) topl))) + ;; If we want Coq pbp: (setq coq-current-goal 1) + (while (setq ip (car topl) + topl (cdr topl)) + (pbp-make-top-span ip (car topl)))))) + +(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-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) + (erase-buffer) + (insert str)) + ((eq ins 'analyse) + (proof-shell-analyse-structure str)) + (t (set-buffer proof-pbp-buffer) + (insert "\n\nbug???"))))) + (run-hooks 'proof-shell-handle-delayed-output-hook) + (setq proof-shell-delayed-output (cons 'insert "done"))) + +(defun proof-shell-handle-error (cmd string) + (save-excursion + (display-buffer (set-buffer proof-pbp-buffer)) + (if (not (eq proof-shell-delayed-output (cons 'insert "done"))) + (progn + (set-buffer proof-pbp-buffer) + (erase-buffer) + (insert (proof-shell-strip-annotations + (cdr proof-shell-delayed-output))))) + (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-detach-queue) + (delete-spans (proof-locked-end) (point-max) 'type) + (proof-release-lock) + (run-hooks 'proof-shell-handle-error-hook)) + +(defun proof-shell-handle-interrupt () + (save-excursion + (display-buffer (set-buffer proof-pbp-buffer)) + (goto-char (point-max)) + (newline 2) + (insert-string + "Interrupt: Script Management may be in an inconsistent state\n") + (beep)) + (set-buffer proof-script-buffer) + (if proof-shell-busy + (progn (proof-detach-queue) + (delete-spans (proof-locked-end) (point-max) 'type) + (proof-release-lock)))) + + +(defun proof-goals-pos (span maparg) + "Given a span, this function returns the start of it if corresponds + to a goal and nil otherwise." + (and (eq 'goal (car (span-property span 'proof-top-element))) + (span-start span))) + +(defun proof-pbp-focus-on-first-goal () + "If the `proof-pbp-buffer' contains goals, the first one is brought + into view." + (and (fboundp 'map-extents) + (let + ((pos (map-extents 'proof-goals-pos proof-pbp-buffer + nil nil nil nil 'proof-top-element))) + (and pos (set-window-point + (get-buffer-window proof-pbp-buffer t) pos))))) + + + +(defun proof-shell-process-output (cmd string) + "Deals with errors, start of proofs, abortions of proofs and + completions of proofs. All other output from the proof engine is + simply reported to the user in the RESPONSE buffer. To extend this + function, set `proof-shell-process-output-system-specific'. + + The basic output processing function - it can return one of 4 + things: 'error, 'interrupt, 'loopback, or nil. 'loopback means this + was output from pbp, and should be inserted into the script buffer + and sent back to the proof assistant." + (cond + ((string-match proof-shell-error-regexp string) + (cons 'error (proof-shell-strip-annotations + (substring string (match-beginning 0))))) + + ((string-match proof-shell-interrupt-regexp string) + 'interrupt) + + ((and proof-shell-abort-goal-regexp + (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))) + (setq end (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)))) + + ;; hook to tailor proof-shell-process-output to a specific proof + ;; system + ((and proof-shell-process-output-system-specific + (funcall (car proof-shell-process-output-system-specific) + cmd string)) + (funcall (cdr proof-shell-process-output-system-specific) + cmd string)) + + (t (setq proof-shell-delayed-output (cons 'insert string))))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Low-level commands for shell communication ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-shell-insert (string) + (set-buffer proof-shell-buffer) + (goto-char (point-max)) + + (run-hooks 'proof-shell-insert-hook) + (insert string) + + ;; xemacs and emacs19 have different semantics for what happens when + ;; shell input is sent next to a marker + ;; the following code accommodates both definitions + (if (marker-position proof-marker) + (let ((inserted (point))) + (comint-send-input) + (set-marker proof-marker inserted)) + (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 (proof-shell-insert string))) + +;; 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 (&optional relaxed) + "Checks + (1) Is a proof process running? + (2) Is the proof process idle? + (3) Does the current buffer own the proof process? + (4) Is the current buffer a proof script? + and signals an error if at least one of the conditions is not + fulfilled. If relaxed is set, only (1) and (2) are tested." + (if (proof-shell-live-buffer) + (cond + (proof-shell-busy (error "Proof Process Busy!")) + (relaxed ()) ;exit cond + ((not (eq proof-script-buffer (current-buffer))) + (error "Don't own proof process")))) + (if (not (or relaxed (eq proof-buffer-type 'script))) + (error "Must be running in a script buffer"))) + +(defun proof-grab-lock (&optional relaxed) + (proof-start-shell) + (proof-check-process-available relaxed) + (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 &optional relaxed) + (if start + (proof-set-queue-endpoints start end)) + (let (item) + (while (and alist (string= + (nth 1 (setq item (car alist))) + "COMMENT")) + (funcall (nth 2 item) (car item)) + (setq alist (cdr alist))) + (if alist + (progn + (proof-grab-lock relaxed) + (setq proof-shell-delayed-output (cons 'insert "Done.")) + (setq proof-action-list alist) + (proof-send (nth 1 item)))))) + +; 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")) + (let ((item (car proof-action-list))) + (funcall (nth 2 item) (car item)) + (setq proof-action-list (cdr proof-action-list)) + (while (and proof-action-list + (string= + (nth 1 (setq item (car proof-action-list))) + "COMMENT")) + (funcall (nth 2 item) (car item)) + (setq proof-action-list (cdr proof-action-list))) + (if (null proof-action-list) + (progn (proof-release-lock) + (proof-detach-queue) + t) + (proof-send (nth 1 item)) + nil)))) + +(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 and indenting)." + (save-excursion + (set-buffer proof-script-buffer) + (let (span) + (proof-goto-end-of-locked) + (newline-and-indent) + (insert cmd) + (setq span (make-span (proof-locked-end) (point))) + (set-span-property span 'type 'pbp) + (set-span-property span 'cmd cmd) + (proof-set-queue-endpoints (proof-locked-end) (point)) + (setq proof-action-list + (cons (car proof-action-list) + (cons (list span cmd 'proof-done-advancing) + (cdr proof-action-list))))))) + +;; ******** NB ********** +;; While we're using pty communication, this code is OK, since all +;; eager annotations are one line long, and we get input a line at a +;; time. If we go over to piped communication, it will break. + +(defun proof-shell-popup-eager-annotation () + "Eager annotations are annotations which the proof system produces +while it's doing something (e.g. loading libraries) to say how much +progress it's made. Obviously we need to display these as soon as they +arrive." + (let (mrk str file module) + (save-excursion + (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)) + (goto-char (point-max)) + (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) + "The filter for the shell-process. We sleep until we get a + wakeup-char in the input, then run proof-shell-process-output, and + set proof-marker to keep track of how far we've got." + (if (string-match proof-shell-eager-annotation-end str) + (proof-shell-popup-eager-annotation)) + (if (or + ;; Some proof systems can be hacked to have annotated prompts; + ;; for these we set proof-shell-wakeup-char to the annotation special. + (and proof-shell-wakeup-char + (string-match (char-to-string proof-shell-wakeup-char) str)) + ;; Others rely on a standard top-level (e.g. SML) whose prompt can't + ;; be hacked. For those we use the prompt regexp. + (string-match proof-shell-annotated-prompt-regexp str)) + (if (null (marker-position proof-marker)) + ;; Set marker to first prompt in output buffer, and sleep again. + (progn + (goto-char (point-min)) + (re-search-forward proof-shell-annotated-prompt-regexp) + ;; FIXME: da: why is this next line here? to delete the + ;; possibly several character prompt? why? + ;; TMS: Its purpose is to remove the wakeup + ;; character associated with the prompt. This + ;; should not be necessary anymore, because the wakeup + ;; character isn't displayed anyway; see + ;; `proof-dont-show-annotations'. Watch this space! + (backward-delete-char 1) + (set-marker proof-marker (point))) + ;; We've matched against a second prompt in str now. Search + ;; the output buffer for the second prompt after the one previously + ;; marked. + (let (string res cmd) + (goto-char (marker-position proof-marker)) + (re-search-forward proof-shell-annotated-prompt-regexp nil t) + (backward-char (- (match-end 0) (match-beginning 0))) + (setq string (buffer-substring (marker-position proof-marker) + (point))) + (goto-char (point-max)) ; da: assumed to be after a prompt? + (backward-delete-char 1) ; da: WHY? nasty assumption. + (setq cmd (nth 1 (car 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))) + ((eq res 'interrupt) + (proof-shell-handle-interrupt)) + ((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-last-goal-or-goalsave () + (save-excursion + (let ((span (span-at-before (proof-locked-end) 'type))) + (while (and span + (not (eq (span-property span 'type) 'goalsave)) + (or (eq (span-property span 'type) 'comment) + (not (funcall proof-goal-command-p + (span-property span 'cmd))))) + (setq span (prev-span span 'type))) + span))) + +;; This needs some work to make it generic, since most of the code +;; doesn't apply to Coq at all. +(defun proof-steal-process () + "This allows us to steal the process if we want to change the buffer + in which script management is running." + (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) + (t + (let ((flist proof-included-files-list) + (file (expand-file-name (buffer-file-name))) span (cmd "")) + (if (string-match "\\(.*\\)\\.." file) (setq file (match-string 1 file))) + (while (and flist (not (string= file (cdr (car 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"))) + (if (not (buffer-name proof-script-buffer)) + (message "Warning: Proof script buffer deleted: proof state may be inconsistent") + (save-excursion + (set-buffer proof-script-buffer) + (setq proof-active-buffer-fake-minor-mode nil) + (setq span (proof-last-goal-or-goalsave)) + ;; This won't work for Coq if we have recursive goals in progress + (if (and span (not (eq (span-property span 'type) 'goalsave))) + (setq cmd proof-kill-goal-command)) + (proof-detach-segments) + (delete-spans (point-min) (point-max) 'type))) + + (setq proof-script-buffer (current-buffer)) + (proof-init-segmentation) + (setq proof-active-buffer-fake-minor-mode t) + + (cond + (flist + (list nil (concat cmd "ForgetMark " (car (car flist)) ";") + `(lambda (span) (setq proof-included-files-list + (quote ,(cdr flist)))))) + ((not (string= cmd "")) + (list nil cmd 'proof-done-invisible)) + (t nil)))))) + +(defun proof-done-invisible (span) ()) + +(defun proof-invisible-command (cmd &optional relaxed) + "Send cmd to the proof process without responding to the user." + (proof-check-process-available relaxed) + (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)) relaxed)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; User Commands ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +; 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 +; (span,command,action) triples. The loop looks like: Execute the +; command, and if it's successful, do action on span. If the +; command's not successful, we bounce the rest of the queue and do +; some error processing. +; +; when a span 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 +; 'comment - denoting a comment +; 'pbp - denoting a span created by pbp +; 'vanilla - denoting any other span. +; 'pbp & 'vanilla spans 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 + +;; proof-assert-until-point, and various gunk for its ;; +;; setup and callback ;; + +;; This code is for nested goals in Coq, and shouldn't affect things +;; in LEGO. It lifts "local" lemmas from inside goals out to top +;; level. + +(defun proof-lift-global (glob-span) + (let (start (next (span-at 1 'type)) str (goal-p nil)) + (while (and next (and (not (eq next glob-span)) (not goal-p))) + (if (and (eq (span-property next 'type) 'vanilla) + (funcall proof-goal-command-p (span-property next 'cmd))) + (setq goal-p t) + (setq next (next-span next 'type)))) + + (if (and next (not (eq next glob-span))) + (progn + (proof-unlock-locked) + (setq str (buffer-substring (span-start glob-span) + (span-end glob-span))) + (delete-region (span-start glob-span) (span-end glob-span)) + (goto-char (span-start next)) + (setq start (point)) + (insert str "\n") + (set-span-endpoints glob-span start (point)) + (set-span-start next (point)) + (proof-lock-unlocked))))) + +;; This is the actual callback for assert-until-point. + +(defun proof-done-advancing (span) + (let ((end (span-end span)) nam gspan next cmd) + (proof-set-locked-end end) + (proof-set-queue-start end) + (setq cmd (span-property span 'cmd)) + (cond + ((eq (span-property span 'type) 'comment) + (set-span-property span 'mouse-face 'highlight)) + ((string-match proof-save-command-regexp cmd) + ;; In coq, we have the invariant that if we've done a save and + ;; there's a top-level declaration then it must be the + ;; associated goal. (Notice that because it's a callback it + ;; must have been approved by the theorem prover.) + (if (string-match proof-save-with-hole-regexp cmd) + (setq nam (match-string 2 cmd))) + (setq gspan span) + (while (or (eq (span-property gspan 'type) 'comment) + (not (funcall proof-goal-command-p + (setq cmd (span-property gspan 'cmd))))) + (setq next (prev-span gspan 'type)) + (delete-span gspan) + (setq gspan next)) + + (if (null nam) + (if (string-match proof-goal-with-hole-regexp + (span-property gspan 'cmd)) + (setq nam (match-string 2 (span-property gspan 'cmd))) + ;; This only works for Coq, but LEGO raises an error if + ;; there's no name. + ;; FIXME: a nonsense for Isabelle. + (setq nam "Unnamed_thm"))) + + (set-span-end gspan end) + (set-span-property gspan 'mouse-face 'highlight) + (set-span-property gspan 'type 'goalsave) + (set-span-property gspan 'name nam) + + (proof-lift-global gspan)) + (t + (set-span-property span 'mouse-face 'highlight) + (if (funcall proof-global-p cmd) + (proof-lift-global span)))))) + +; depth marks number of nested comments. quote-parity is false if +; we're inside ""'s. Only one of (depth > 0) and (not quote-parity) +; should be true at once. -- hhg + +(defun proof-segment-up-to (pos) + "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." + (save-excursion + (let ((str (make-string (- (buffer-size) (proof-locked-end) -10) ?x)) + (i 0) (depth 0) (quote-parity t) 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)) + (if (not quote-parity) + (message "Warning: unclosed quote")) + (setq done t)) + ((and (looking-at "\\*)") quote-parity) + (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)))) + ((and (looking-at "(\\*") quote-parity) + (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))) + (if (looking-at "\"") + (setq quote-parity (not quote-parity))) + (forward-char) + (if (and (= c proof-terminal-char) quote-parity) + (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 &optional callback-fn) + "Convert a sequence of semicolon positions (returned by the above +function) to a set of vanilla extents." + (let ((ct (proof-locked-end)) span alist semi) + (while (not (null semis)) + (setq semi (car semis) + span (make-span ct (nth 2 semi)) + ct (nth 2 semi)) + (if (eq (car (car semis)) 'cmd) + (progn + (set-span-property span 'type 'vanilla) + (set-span-property span 'cmd (nth 1 semi)) + (setq alist (cons (list span (nth 1 semi) + (or callback-fn 'proof-done-advancing)) + alist))) + (set-span-property span 'type 'comment) + (setq alist (cons (list span "COMMENT" 'proof-done-advancing) alist))) + (setq semis (cdr semis))) + (nreverse alist))) + +; Assert until point - We actually use this to implement the +; assert-until-point, active terminator keypress, and find-next-terminator. +; In different cases we want different things, but usually the information +; (i.e. are we inside a comment) isn't available until we've actually run +; proof-segment-up-to (point), hence all the different options when we've +; done so. + +(defun proof-assert-until-point + (&optional unclosed-comment-fun ignore-proof-process-p) + "Process the region from the end of the locked-region until point. + Default action if inside a comment is just to go until the start of + the comment. If you want something different, put it inside + unclosed-comment-fun. If ignore-proof-process-p is set, no commands + will be added to the queue." + (interactive) + (let ((pt (point)) + (crowbar (or ignore-proof-process-p (proof-steal-process))) + semis) + (save-excursion + (if (not (re-search-backward "\\S-" (proof-locked-end) t)) + (progn (goto-char pt) + (error "Nothing to do!"))) + (setq semis (proof-segment-up-to (point)))) + (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis))) + (funcall unclosed-comment-fun) + (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis))) + (if (and (not ignore-proof-process-p) (not crowbar) (null semis)) + (error "Nothing to do!")) + (goto-char (nth 2 (car semis))) + (and (not ignore-proof-process-p) + (let ((vanillas (proof-semis-to-vanillas (nreverse semis)))) + (if crowbar (setq vanillas (cons crowbar vanillas))) + (proof-start-queue (proof-locked-end) (point) vanillas)))))) + +;; insert-pbp-command - an advancing command, for use when ;; +;; PbpHyp or Pbp has executed in LEGO, and returned a ;; +;; command for us to run ;; + +(defun proof-insert-pbp-command (cmd) + (proof-check-process-available) + (let (span) + (proof-goto-end-of-locked) + (insert cmd) + (setq span (make-span (proof-locked-end) (point))) + (set-span-property span 'type 'pbp) + (set-span-property span 'cmd cmd) + (proof-start-queue (proof-locked-end) (point) + (list (list span cmd 'proof-done-advancing))))) + + +;; proof-retract-until-point and associated gunk ;; +;; most of the hard work (i.e computing the commands to do ;; +;; the retraction) is implemented in the customisation ;; +;; module (lego.el or coq.el) which is why this looks so ;; +;; straightforward ;; + + +(defun proof-done-retracting (span) + "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 span)) + (end (span-end span)) + (kill (span-property span 'delete-me))) + (proof-set-locked-end start) + (proof-set-queue-end start) + (delete-spans start end 'type) + (delete-span span) + (if kill (delete-region start end)))) + +(defun proof-setup-retract-action (start end proof-command delete-region) + (let ((span (make-span start end))) + (set-span-property span 'delete-me delete-region) + (list (list span proof-command 'proof-done-retracting)))) + +(defun proof-retract-target (target delete-region) + (let ((end (proof-locked-end)) + (start (span-start target)) + (span (proof-last-goal-or-goalsave)) + actions) + + (if (and span (not (eq (span-property span 'type) 'goalsave))) + (if (< (span-end span) (span-end target)) + (progn + (setq span target) + (while (and span (eq (span-property span 'type) 'comment)) + (setq span (next-span span 'type))) + (setq actions (proof-setup-retract-action + start end + (if (null span) "COMMENT" + (funcall proof-count-undos-fn span)) + delete-region) + end start)) + + (setq actions (proof-setup-retract-action (span-start span) end + proof-kill-goal-command + delete-region) + end (span-start span)))) + + (if (> end start) + (setq actions + (nconc actions (proof-setup-retract-action + start end + (funcall proof-find-and-forget-fn target) + delete-region)))) + + (proof-start-queue (min start end) (proof-locked-end) actions))) + +(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. If + this function is invoked outside a locked region, the last + successfully processed command is undone." + (interactive) + (proof-check-process-available) + (let ((span (span-at (point) 'type))) + (if (null (proof-locked-end)) (error "No locked region")) + (and (null span) + (progn (proof-goto-end-of-locked) (backward-char) + (setq span (span-at (point) 'type)))) + (proof-retract-target span delete-region))) + +;; proof-try-command ;; +;; this isn't really in the spirit of script management, ;; +;; but sometimes the user wants to just try an expression ;; +;; without having to undo it in order to try something ;; +;; different. Of course you can easily lose sync by doing ;; +;; something here which changes the proof state ;; + +(defun proof-done-trying (span) + (delete-span span) + (proof-detach-queue)) + +(defun proof-try-command + (&optional unclosed-comment-fun) + + "Process the command at point, + but don't add it to the locked region. This will only happen if + the command satisfies proof-state-preserving-p. + + Default action if inside a comment is just to go until the start of + the comment. If you want something different, put it inside + unclosed-comment-fun." + (interactive) + (let ((pt (point)) semis crowbar test) + (setq crowbar (proof-steal-process)) + (save-excursion + (if (not (re-search-backward "\\S-" (proof-locked-end) t)) + (progn (goto-char pt) + (error "Nothing to do!"))) + (setq semis (proof-segment-up-to (point)))) + (if (and unclosed-comment-fun (eq 'unclosed-comment (car semis))) + (funcall unclosed-comment-fun) + (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis))) + (if (and (not crowbar) (null semis)) (error "Nothing to do!")) + (setq test (car semis)) + (if (not (funcall proof-state-preserving-p (nth 1 test))) + (error "Command is not state preserving")) + (goto-char (nth 2 test)) + (let ((vanillas (proof-semis-to-vanillas (list test) + 'proof-done-trying))) + (if crowbar (setq vanillas (cons crowbar vanillas))) + (proof-start-queue (proof-locked-end) (point) vanillas))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; misc other user functions ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(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-locked-end) 'type))) + (proof-retract-until-point t)) + +(defun proof-interrupt-process () + (interactive) + (if (not (proof-shell-live-buffer)) + (error "Proof Process Not Started!")) + (if (not (eq proof-script-buffer (current-buffer))) + (error "Don't own process!")) + (if (not proof-shell-busy) + (error "Proof Process Not Active!")) + (save-excursion + (set-buffer proof-shell-buffer) + (comint-interrupt-subjob))) + + +(defun proof-find-next-terminator () + "Set point after next `proof-terminal-char'." + (interactive) + (let ((cmd (span-at (point) 'type))) + (if cmd (goto-char (span-end cmd)) + (and (re-search-forward "\\S-" nil t) + (proof-assert-until-point nil 'ignore-proof-process))))) + +(defun proof-process-buffer () + "Process the current buffer and set point at the end of the buffer." + (interactive) + (end-of-buffer) + (proof-assert-until-point)) + +;; For when things go horribly wrong + +(defun proof-restart-script () + (interactive) + (save-excursion + (if (buffer-live-p proof-script-buffer) + (progn + (set-buffer proof-script-buffer) + (setq proof-active-buffer-fake-minor-mode nil) + (delete-spans (point-min) (point-max) 'type) + (proof-detach-segments))) + (setq proof-shell-busy nil + proof-script-buffer nil) + (if (buffer-live-p proof-shell-buffer) + (kill-buffer proof-shell-buffer)) + (if (buffer-live-p proof-pbp-buffer) + (kill-buffer proof-pbp-buffer)))) + +;; A command for making things go horribly wrong - it moves the +;; end-of-locked-region marker backwards, so user had better move it +;; correctly to sync with the proof state, or things will go all +;; pear-shaped. + +(defun proof-frob-locked-end () + (interactive) + "Move the end of the locked region backwards. + Only for use by consenting adults." + (cond + ((not (eq proof-script-buffer (current-buffer))) + (error "Not in proof buffer")) + ((> (point) (proof-locked-end)) + (error "Can only move backwards")) + (t (proof-set-locked-end (point)) + (delete-spans (proof-locked-end) (point-max) 'type)))) + +(defvar proof-minibuffer-history nil + "The last command read from the minibuffer") + +(defun proof-execute-minibuffer-cmd () + (interactive) + (let (cmd) + (proof-check-process-available 'relaxed) + (setq cmd (read-string "Command: " nil 'proof-minibuffer-history)) + (proof-invisible-command cmd 'relaxed))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;;; Popup and Pulldown Menu ;;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;;; Menu commands for the underlying proof assistant +(defvar proof-ctxt-string "" + "Command to display context in proof assistant") + +(defvar proof-help-string "" + "Command to ask for help in proof assistant") + +(defvar proof-prf-string "" + "Command to display proof state in proof assistant") + +(defun proof-ctxt () + "List context." + (interactive) + (proof-invisible-command (concat proof-ctxt-string proof-terminal-string))) + +(defun proof-help () + "Print help message giving syntax." + (interactive) + (proof-invisible-command (concat proof-help-string proof-terminal-string))) + +(defun proof-prf () + "List proof state." + (interactive) + (proof-invisible-command (concat proof-prf-string proof-terminal-string))) + +;;; To be called from menu +(defun proof-info-mode () + "Info mode on proof mode." + (interactive) + (info "script-management")) + +(defun proof-exit () + "Exit Proof-assistant." + (interactive) + (proof-restart-script)) + +(defvar proof-help-menu + '("Help" + ["Proof assistant web page" + (w3-fetch proof-www-home-page) t] + ["Help on Emacs proof-mode" proof-info-mode t] + ) + "The Help Menu in Script Management.") + +(defvar proof-shared-menu + (append-element '( + ["Display context" proof-ctxt + :active (proof-shell-live-buffer)] + ["Display proof state" proof-prf + :active (proof-shell-live-buffer)] + ["Exit proof assistant" proof-exit + :active (proof-shell-live-buffer)] + "----" + ["Find definition/declaration" find-tag-other-window t] + ) + proof-help-menu)) + +(defvar proof-menu + (append '("Commands" + ["Toggle active terminator" proof-active-terminator-minor-mode + :active t + :style toggle + :selected proof-active-terminator-minor-mode] + "----") + (list (if (string-match "XEmacs 19.1[2-9]" emacs-version) + "--:doubleLine" "----")) + proof-shared-menu + ) + "*The menu for the proof assistant.") + +(defvar proof-shell-menu proof-shared-menu + "The menu for the Proof-assistant shell") + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Active terminator minor mode ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(deflocal proof-active-terminator-minor-mode nil + "active terminator minor mode flag") + +(defun proof-active-terminator-minor-mode (&optional arg) + "Toggle PROOF's Active Terminator minor mode. +With arg, turn on the Active Terminator minor mode if and only if arg +is positive. + +If Active terminator mode is enabled, a terminator will process the +current command." + + (interactive "P") + +;; has this minor mode been registered as such? + (or (assq 'proof-active-terminator-minor-mode minor-mode-alist) + (setq minor-mode-alist + (append minor-mode-alist + (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))) + +(defun proof-process-active-terminator () + "Insert the terminator in an intelligent way and assert until the + new terminator. Fire up proof process if necessary." + (let ((mrk (point)) ins) + (if (looking-at "\\s-\\|\\'\\|\\w") + (if (not (re-search-backward "\\S-" (proof-unprocessed-begin) t)) + (error "Nothing to do!"))) + (if (not (= (char-after (point)) proof-terminal-char)) + (progn (forward-char) (insert proof-terminal-string) (setq ins t))) + (proof-assert-until-point + (function (lambda () + (if ins (backward-delete-char 1)) + (goto-char mrk) (insert proof-terminal-string)))))) + +(defun proof-active-terminator () + (interactive) + (if proof-active-terminator-minor-mode + (proof-process-active-terminator) + (self-insert-command 1))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Proof mode configuration ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + +(define-derived-mode proof-mode fundamental-mode + proof-mode-name "Proof mode - not standalone" + ;; define-derived-mode proof-mode initialises proof-mode-map + (setq proof-buffer-type 'script)) + +;; This has to come after proof-mode is defined + +(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) + (setq comint-get-old-input (function (lambda () ""))) + (proof-dont-show-annotations) + (setq proof-marker (make-marker))) + +(easy-menu-define proof-shell-menu + proof-shell-mode-map + "Menu used in the proof assistant shell." + (cons proof-mode-name (cdr proof-shell-menu))) + +(easy-menu-define proof-mode-menu + proof-mode-map + "Menu used in proof mode." + (cons proof-mode-name (cdr proof-menu))) + +;; the following callback is an irritating hack - there should be some +;; elegant mechanism for computing constants after the child has +;; configured. + +(defun proof-config-done () + +;; calculate some strings and regexps for searching + + (setq proof-terminal-string (char-to-string proof-terminal-char)) + + (setq pbp-goal-command (concat "Pbp %s" proof-terminal-string)) + (setq pbp-hyp-command (concat "PbpHyp %s" proof-terminal-string)) + + (make-local-variable 'comment-start) + (setq comment-start (concat proof-comment-start " ")) + (make-local-variable 'comment-end) + (setq comment-end (concat " " proof-comment-end)) + (make-local-variable 'comment-start-skip) + (setq comment-start-skip + (concat (regexp-quote proof-comment-start) "+\\s_?")) + + (setq proof-re-end-of-cmd (concat "\\s_*" proof-terminal-string "\\s_*\\\'")) + (setq proof-re-term-or-comment + (concat proof-terminal-string "\\|" (regexp-quote proof-comment-start) + "\\|" (regexp-quote proof-comment-end))) + +;; func-menu --- Jump to a goal within a buffer + (and (boundp 'fume-function-name-regexp-alist) + (defvar fume-function-name-regexp-proof + (cons proof-goal-with-hole-regexp 2)) + (push (cons major-mode 'fume-function-name-regexp-proof) + fume-function-name-regexp-alist)) + (and (boundp 'fume-find-function-name-method-alist) + (push (cons major-mode 'fume-match-find-next-function-name) + fume-find-function-name-method-alist)) + +;; Info + (or (memq proof-info-dir Info-default-directory-list) + (setq Info-default-directory-list + (cons proof-info-dir Info-default-directory-list))) + +;; keymaps and menus + (easy-menu-add proof-mode-menu proof-mode-map) + + (proof-define-keys proof-mode-map proof-universal-keys) + + (define-key proof-mode-map + (vconcat [(control c)] (vector proof-terminal-char)) + 'proof-active-terminator-minor-mode) + + (define-key proof-mode-map [(control c) (control e)] + 'proof-find-next-terminator) + + (define-key proof-mode-map (vector proof-terminal-char) + 'proof-active-terminator) + (define-key proof-mode-map [(control c) (return)] 'proof-assert-until-point) + (define-key proof-mode-map [(control c) (control t)] 'proof-try-command) + (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-interactive) + (define-key proof-mode-map [(control button1)] 'proof-send-span) + (define-key proof-mode-map [(control c) (control b)] 'proof-process-buffer) + (define-key proof-mode-map [(control c) (control z)] 'proof-frob-locked-end) + + (define-key proof-mode-map [tab] 'proof-indent-line) + (make-local-variable 'indent-line-function) + (setq indent-line-function 'proof-indent-line) + + (define-key (current-local-map) [(control c) (control p)] 'proof-prf) + (define-key (current-local-map) [(control c) ?c] 'proof-ctxt) + (define-key (current-local-map) [(control c) ?h] 'proof-help) + +;; 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. + + (and (boundp 'font-lock-always-fontify-immediately) + (setq font-lock-always-fontify-immediately t)) + + (run-hooks 'proof-mode-hook)) + +(defun proof-shell-config-done () + (accept-process-output (get-buffer-process (current-buffer))) + + ;; If the proof process in invoked on a different machine e.g., + ;; for proof-prog-name="rsh fastmachine proofprocess", one needs + ;; to adjust the directory: + (and proof-shell-cd + (proof-shell-insert (format proof-shell-cd + ;; under Emacs 19.34 default-directory contains "~" which causes + ;; problems with LEGO's internal Cd command + (expand-file-name default-directory)))) + + (if proof-shell-init-cmd + (proof-shell-insert proof-shell-init-cmd)) + +;; Note that proof-marker actually gets set in proof-shell-filter. +;; This is manifestly a hack, but finding somewhere more convenient +;; to do the setup is tricky. + + (while (null (marker-position proof-marker)) + (if (accept-process-output (get-buffer-process (current-buffer)) 15) + () + (error "Failed to initialise proof process")))) + +(define-derived-mode pbp-mode fundamental-mode + proof-mode-name "Proof by Pointing" + ;; defined-derived-mode pbp-mode initialises pbp-mode-map + (setq proof-buffer-type 'pbp) + (suppress-keymap pbp-mode-map 'all) +; (define-key pbp-mode-map [(button2)] 'pbp-button-action) + (proof-define-keys pbp-mode-map proof-universal-keys) + (erase-buffer)) + + +(provide 'proof) diff --git a/generic/span-extent.el b/generic/span-extent.el new file mode 100644 index 00000000..6e6183cd --- /dev/null +++ b/generic/span-extent.el @@ -0,0 +1,82 @@ +;;; This file implements spans in terms of extents, for xemacs. +;;; Copyright (C) 1998 LFCS Edinburgh +;;; Author: Healfdene Goguen + +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> + +;; $Log$ +;; Revision 1.1 1998/09/03 13:51:33 da +;; Renamed for new subdirectory structure +;; +;; Revision 2.0 1998/08/11 15:00:13 da +;; New branch +;; +;; Revision 1.4 1998/06/10 14:01:48 hhg +;; Wrote generic span functions for making spans read-only or read-write. +;; +;; Revision 1.3 1998/06/02 15:36:44 hhg +;; Corrected comment about this being for xemacs. +;; +;; Revision 1.2 1998/05/19 15:30:27 hhg +;; Added header and log message. +;; + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Bridging the emacs19/xemacs gulf ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Now define "spans" in terms of extents. + +(defsubst make-span (start end) + (make-extent start end)) + +(defsubst detach-span (span) + (detach-extent span)) + +(defsubst set-span-endpoints (span start end) + (set-extent-endpoints span start end)) + +(defsubst set-span-start (span value) + (set-extent-endpoints span value (extent-end-position span))) + +(defsubst set-span-end (span value) + (set-extent-endpoints span (extent-start-position span) value)) + +(defsubst span-read-only (span) + (set-span-property span 'read-only t)) + +(defsubst span-read-write (span) + (set-span-property span 'read-only nil)) + +(defsubst span-property (span name) + (extent-property span name)) + +(defsubst set-span-property (span name value) + (set-extent-property span name value)) + +(defsubst delete-span (span) + (delete-extent span)) + +(defsubst delete-spans (start end prop) + (mapcar-extents 'delete-extent nil (current-buffer) start end nil prop)) + +(defsubst span-at (pt prop) + (extent-at pt nil prop)) + +(defsubst span-at-before (pt prop) + (extent-at pt nil prop nil 'before)) + +(defsubst span-start (span) + (extent-start-position span)) + +(defsubst span-end (span) + (extent-end-position span)) + +(defsubst prev-span (span prop) + (extent-at (extent-start-position span) nil prop nil 'before)) + +(defsubst next-span (span prop) + (extent-at (extent-end-position span) nil prop nil 'after)) + + +(provide 'span-extent) diff --git a/generic/span-overlay.el b/generic/span-overlay.el new file mode 100644 index 00000000..e67ad33c --- /dev/null +++ b/generic/span-overlay.el @@ -0,0 +1,291 @@ +;;; This file implements spans in terms of overlays, for emacs19. +;;; Copyright (C) 1998 LFCS Edinburgh +;;; Author: Healfdene Goguen + +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> + +;; $Log$ +;; Revision 1.1 1998/09/03 13:51:34 da +;; Renamed for new subdirectory structure +;; +;; Revision 2.0 1998/08/11 15:00:13 da +;; New branch +;; +;; Revision 1.9 1998/06/10 14:02:39 hhg +;; Wrote generic span functions for making spans read-only or read-write. +;; Fixed bug in add-span and remove-span concerning return value of +;; span-traverse. +;; +;; Revision 1.8 1998/06/10 12:41:47 hhg +;; Compare span-end first rather than span-start in span-lt, because +;; proof-lock-span is often changed and has starting point 1. +;; Factored out common code of add-span and remove-span into +;; span-traverse. +;; +;; Revision 1.7 1998/06/03 17:40:07 hhg +;; Changed last-span to before-list. +;; Added definitions of foldr and foldl if they aren't already loaded. +;; Changed definitions of add-span, remove-span and find-span-aux to be +;; non-recursive. +;; Removed detach-extent since this file isn't used by xemacs. +;; Added function append-unique to avoid repetitions in list generated by +;; spans-at-region. +;; Changed next-span so it uses member-if. +;; +;; Revision 1.6 1998/06/02 15:36:51 hhg +;; Corrected comment about this being for emacs19. +;; +;; Revision 1.5 1998/05/29 09:50:10 tms +;; o outsourced indentation to proof-indent +;; o support indentation of commands +;; o replaced test of Emacs version with availability test of specific +;; features +;; o C-c C-c, C-c C-v and M-tab is now available in all buffers +;; +;; Revision 1.4 1998/05/21 17:27:41 hhg +;; Removed uninitialized os variable in spans-at-region. +;; +;; Revision 1.3 1998/05/21 08:28:52 hhg +;; Initialize 'before pointer in add-span-aux when last-span is nil. +;; Removed span-at-type. +;; Fixed bug in span-at-before, where (span-start span) may be nil. +;; Added spans-at-(point|region)[-prop], which fixes bug of C-c u at end +;; of buffer. +;; +;; Revision 1.2 1998/05/19 15:31:37 hhg +;; Added header and log message. +;; Fixed set-span-endpoints so it preserves invariant. +;; Changed add-span and remove-span so that they update last-span +;; correctly themselves, and don't take last-span as an argument. +;; + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Bridging the emacs19/xemacs gulf ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; before-list represents a linked list of spans for each buffer. +;; It has the invariants of: +;; * being ordered wrt the starting point of the spans in the list, +;; with detached spans at the end. +;; * not having overlapping overlays of the same type. + +(defvar before-list nil + "Start of backwards-linked list of spans") + +(make-variable-buffer-local 'before-list) + + +(or (fboundp 'foldr) +(defun foldr (func a seq) + "Return (func (func (func (... (func a Sn) ...) S2) S1) S0) +when func's argument is 2 and seq is a sequence whose +elements = S0 S1 S2 ... Sn. [tl-seq.el]" + (let ((i (length seq))) + (while (> i 0) + (setq i (1- i)) + (setq a (funcall func a (elt seq i))) + ) + a))) + +(or (fboundp 'foldl) +(defun foldl (func a seq) + "Return (... (func (func (func a S0) S1) S2) ...) +when func's argument is 2 and seq is a sequence whose +elements = S0 S1 S2 .... [tl-seq.el]" + (let ((len (length seq)) + (i 0)) + (while (< i len) + (setq a (funcall func a (elt seq i))) + (setq i (1+ i)) + ) + a))) + +(defsubst span-start (span) + (overlay-start span)) + +(defsubst span-end (span) + (overlay-end span)) + +(defun set-span-property (span name value) + (overlay-put span name value)) + +(defsubst span-property (span name) + (overlay-get span name)) + +(defun span-read-only-hook (overlay after start end &optional len) + (error "Region is read-only")) + +(defun span-read-only (span) + (set-span-property span 'modification-hooks '(span-read-only-hook)) + (set-span-property span 'insert-in-front-hooks '(span-read-only-hook))) + +(defun span-read-write (span) + (set-span-property span 'modification-hooks nil) + (set-span-property span 'insert-in-front-hooks nil)) + +(defun int-nil-lt (m n) + (cond + ((eq m n) nil) + ((not n) t) + ((not m) nil) + (t (< m n)))) + +;; We use end first because proof-locked-queue is often changed, and +;; its starting point is always 1 +(defun span-lt (s u) + (or (int-nil-lt (span-end s) (span-end u)) + (and (eq (span-end s) (span-end u)) + (int-nil-lt (span-start s) (span-start u))))) + +(defun span-traverse (span prop) + (cond + ((not before-list) + ;; before-list empty + 'empty) + ((funcall prop before-list span) + ;; property holds for before-list and span + 'hd) + (t + ;; traverse before-list for property + (let ((l before-list) (before (span-property before-list 'before))) + (while (and before (not (funcall prop before span))) + (setq l before) + (setq before (span-property before 'before))) + l)))) + +(defun add-span (span) + (let ((ans (span-traverse span 'span-lt))) + (cond + ((eq ans 'empty) + (set-span-property span 'before nil) + (setq before-list span)) + ((eq ans 'hd) + (set-span-property span 'before before-list) + (setq before-list span)) + (t + (set-span-property span 'before + (span-property ans 'before)) + (set-span-property ans 'before span))))) + +(defun make-span (start end) + (add-span (make-overlay start end))) + +(defun remove-span (span) + (let ((ans (span-traverse span 'eq))) + (cond + ((eq ans 'empty) + (error "Bug: empty span list")) + ((eq ans 'hd) + (setq before-list (span-property before-list 'before))) + (ans + (set-span-property ans 'before (span-property span 'before))) + (t (error "Bug: span does not occur in span list"))))) + +;; extent-at gives "smallest" extent at pos +;; we're assuming right now that spans don't overlap +(defun spans-at-point (pt) + (let ((overlays nil) (os nil)) + (setq os (overlays-at pt)) + (while os + (if (not (memq (car os) overlays)) + (setq overlays (cons (car os) overlays))) + (setq os (cdr os))) + overlays)) + +;; assumes that there are no repetitions in l or m +(defun append-unique (l m) + (foldl (lambda (n a) (if (memq a m) n (cons a n))) m l)) + +(defun spans-at-region (start end) + (let ((overlays nil) (pos start)) + (while (< pos end) + (setq overlays (append-unique (spans-at-point pos) overlays)) + (setq pos (next-overlay-change pos))) + overlays)) + +(defun spans-at-point-prop (pt prop) + (let ((f (cond + (prop (lambda (spans span) + (if (span-property span prop) (cons span spans) + spans))) + (t (lambda (spans span) (cons span spans)))))) + (foldl f nil (spans-at-point pt)))) + +(defun spans-at-region-prop (start end prop) + (let ((f (cond + (prop (lambda (spans span) + (if (span-property span prop) (cons span spans) + spans))) + (t (lambda (spans span) (cons span spans)))))) + (foldl f nil (spans-at-region start end)))) + +(defun span-at (pt prop) + (car (spans-at-point-prop pt prop))) + +(defsubst detach-span (span) + (remove-span span) + (delete-overlay span) + (add-span span)) + +(defsubst delete-span (span) + (remove-span span) + (delete-overlay span)) + +;; The next two change ordering of list of spans: +(defsubst set-span-endpoints (span start end) + (remove-span span) + (move-overlay span start end) + (add-span span)) + +(defsubst set-span-start (span value) + (set-span-endpoints span value (span-end span))) + +;; This doesn't affect invariant: +(defsubst set-span-end (span value) + (set-span-endpoints span (span-start span) value)) + +(defsubst delete-spans (start end prop) + (mapcar 'delete-span (spans-at-region-prop start end prop))) + +(defun map-spans-aux (f l) + (cond (l (cons (funcall f l) (map-spans-aux f (span-property l 'before)))) + (t ()))) + +(defsubst map-spans (f) + (map-spans-aux f before-list)) + +(defun find-span-aux (prop-p l) + (while (and l (not (funcall prop-p l))) + (setq l (span-property l 'before))) + l) + +(defun find-span (prop-p) + (find-span-aux prop-p before-list)) + +(defun span-at-before (pt prop) + (let ((prop-pt-p + (cond (prop (lambda (span) + (let ((start (span-start span))) + (and start (> pt start) + (span-property span prop))))) + (t (lambda (span) + (let ((start (span-start span))) + (and start (> pt start)))))))) + (find-span prop-pt-p))) + +(defun prev-span (span prop) + (let ((prev-prop-p + (cond (prop (lambda (span) (span-property span prop))) + (t (lambda (span) t))))) + (find-span-aux prev-prop-p (span-property span 'before)))) + +;; overlays are [start, end) +;; If there are two spans overlapping then this won't work. +(defun next-span (span prop) + (let ((l (member-if (lambda (span) (span-property span prop)) + (overlays-at + (next-overlay-change (overlay-start span)))))) + (if l (car l) nil))) + + +(provide 'span-overlay) |