diff options
Diffstat (limited to 'generic/proof-script.el')
-rw-r--r-- | generic/proof-script.el | 697 |
1 files changed, 30 insertions, 667 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 1e2c50aa..634cf644 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -12,6 +12,7 @@ (require 'proof) ; loader (require 'proof-syntax) ; utils for manipulating syntax (require 'span) ; abstraction of overlays/extents +(require 'pg-user) ; user-level commands (require 'proof-menu) ; menus for script mode @@ -111,6 +112,31 @@ proof-script-next-entity-regexps, which see." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; da FIXME: clean this section +;; Notes on markup in the scripting buffer. (da) +;; +;; The locked region is covered by a collection of non-overlaping +;; spans (our abstraction of extents/overlays). +;; +;; For an unfinished proof, there is one extent for each command +;; or comment outside a command. For a finished proof, there +;; is one extent for the whole proof. +;; +;; Each command span has a 'type property, one of: +;; +;; 'proof A goal..savegoal region in the buffer, a completed proof. +;; 'vanilla Initialised in proof-semis-to-vanillas, for +;; 'comment A comment outside a command. +;; 'proverproc A region closed by the prover, processed outwith PG +;; 'pbp A PBP command inserted automatically into the script +;; +;; All spans except those of type 'comment have a 'cmd property, +;; which is set to a string of its command. This is the +;; text in the buffer stripped of leading whitespace and any comments. +;; +;; + + + (deflocal proof-locked-span nil "The locked span of the buffer. Each script buffer has its own locked span, which may be detached @@ -338,9 +364,9 @@ If interactive or SWITCH is non-nil, switch to script buffer first." (interactive) (proof-with-script-buffer (if (and (not (get-buffer-window proof-script-buffer)) - (or switch (and (interactive-p) proof-script-buffer)) - (switch-to-buffer proof-script-buffer)) - (goto-char (proof-unprocessed-begin))))) + (or switch (interactive-p))) + (switch-to-buffer proof-script-buffer) + (goto-char (proof-unprocessed-begin))))) ; NB: think about this because the movement can happen when the user ; is typing, not very nice! @@ -1955,263 +1981,7 @@ command." - - - - -;; -;; User-level functions. -;; -;; TODO: put these in a new file, proof-user, which defines -;; user-level scripting mode. Or put stuff above in a new -;; file, proof-core.el for low-level scripting functions. -;; - - -;; First a couple of helper functions - -(defmacro proof-maybe-save-point (&rest body) - "Save point according to proof-follow-mode, execute BODY." - `(if (eq proof-follow-mode 'locked) - (progn - ,@body) - (save-excursion - ,@body))) - -(defun proof-maybe-follow-locked-end () - "Maybe point to the make sure the locked region is displayed." - (if (eq proof-follow-mode 'follow) - (proof-goto-end-of-queue-or-locked-if-not-visible))) - - -;; -;; Doing commands -;; - -(defun proof-assert-next-command-interactive () - "Process until the end of the next unprocessed command after point. -If inside a comment, just process until the start of the comment." - (interactive) - (proof-with-script-buffer - (proof-maybe-save-point - (goto-char (proof-queue-or-locked-end)) - (proof-assert-next-command)) - (proof-maybe-follow-locked-end))) - -(defun proof-process-buffer () - "Process the current (or script) buffer, and maybe move point to the end." - (interactive) - (proof-with-script-buffer - (proof-maybe-save-point - (goto-char (point-max)) - (proof-assert-until-point-interactive)) - (proof-maybe-follow-locked-end))) - - -;; -;; Undoing commands -;; - -(defun proof-undo-last-successful-command () - "Undo last successful command at end of locked region." - (interactive) - (proof-undo-last-successful-command-1)) - -(defun proof-undo-and-delete-last-successful-command () - "Undo and delete last successful command at end of locked region. -Useful if you typed completely the wrong command. -Also handy for proof by pointing, in case the last proof-by-pointing -command took the proof in a direction you don't like. - -Notice that the deleted command is put into the Emacs kill ring, so -you can use the usual `yank' and similar commands to retrieve the -deleted text." - (interactive) - (proof-undo-last-successful-command-1 'delete) - ;; FIXME want to do this here for 3.3, for nicer behaviour - ;; when deleting. - ;; Unfortunately nasty problem with read only flag when - ;; inserting at (proof-locked-end) sometimes behaves as if - ;; point is inside locked region (prob because span is - ;; [ ) and not [ ] -- why??). - ;; (proof-script-new-command-advance) - ) - -;; No direct key-binding for this one: C-c C-u was too dangerous, -;; when used quickly it's too easy to accidently delete! -(defun proof-undo-last-successful-command-1 (&optional delete) - "Undo last successful command at end of locked region. -If optional DELETE is non-nil, the text is also deleted from -the proof script." - (interactive "P") - (proof-with-script-buffer - (proof-maybe-save-point - (unless (proof-locked-region-empty-p) - (let ((lastspan (span-at-before (proof-locked-end) 'type))) - (if lastspan - (progn - (goto-char (span-start lastspan)) - (proof-retract-until-point delete)) - (error "Nothing to undo!"))))) - (proof-maybe-follow-locked-end))) - -(defun proof-retract-buffer () - "Retract the current buffer, and maybe move point to the start." - (interactive) - (proof-with-script-buffer - (proof-maybe-save-point - (goto-char (point-min)) - (proof-retract-until-point-interactive)) - (proof-maybe-follow-locked-end))) - -(defun proof-retract-current-goal () - "Retract the current proof, and move point to its start." - (interactive) - (proof-maybe-save-point - (let - ((span (proof-last-goal-or-goalsave))) - (if (and span (not (eq (span-property span 'type) 'goalsave)) - (< (span-end span) (proof-unprocessed-begin))) - (progn - (goto-char (span-start span)) - (proof-retract-until-point-interactive) - (proof-maybe-follow-locked-end)) - (error "Not proving"))))) - -;; -;; Interrupt -;; - -(defun proof-interrupt-process () - "Interrupt the proof assistant. Warning! This may confuse Proof General. -This sends an interrupt signal to the proof assistant, if Proof General -thinks it is busy. - -This command is risky because when an interrupt is trapped in the -proof assistant, we don't know whether the last command succeeded or -not. The assumption is that it didn't, which should be true most of -the time, and all of the time if the proof assistant has a careful -handling of interrupt signals." - (interactive) - (unless (proof-shell-live-buffer) - (error "Proof Process Not Started!")) - (unless proof-shell-busy - (error "Proof Process Not Active!")) - (with-current-buffer proof-shell-buffer - ;; Just send an interrrupt. - ;; Action on receiving one is triggered in proof-shell - (comint-interrupt-subjob) - (run-hooks 'proof-shell-pre-interrupt-hook))) - - -;; -;; Movement commands -;; - -;; FIXME da: the next function is messy. Also see notes in 'todo' -(defun proof-goto-command-start () - "Move point to start of current (or final) command of the script." - (interactive) - (let* ((cmd (span-at (point) 'type)) - (start (if cmd (span-start cmd)))) - (if start - (progn - ;; BUG: only works for unclosed proofs. - (goto-char start)) - (let ((semis (nth 1 (proof-segment-up-to (point) t)))) - (if (eq 'unclosed-comment (car-safe semis)) - (setq semis (cdr-safe semis))) - (if (nth 2 semis) ; fetch end point of previous command - (goto-char (nth 2 semis)) - ;; no previous command: just next to end of locked - (goto-char (proof-locked-end))))) - ;; Oddities of this function: if we're beyond the last proof - ;; command, it jumps back to the last command. Could alter this - ;; by spotting that command end of last of semis is before - ;; point. Also, behaviour with comments is different depending - ;; on whether locked or not. - (skip-chars-forward " \t\n"))) - -;; FIXME!! UNIFNISHED -;(defun proof-forward-command (&optional arg) -; "Move forward to end of next command. With argument, repeat. -;With negative argument, move backward repeatedly." -; (interactive "p") -; (or arg (setq arg 1)) -; (if (< arg 0) -; (proof-backward-command (- arg)) - -;; FIXME: these aren't quite the functions I want yet -(defalias 'proof-forward-command 'proof-goto-command-start) -(defalias 'proof-backward-command 'proof-goto-command-end) - -(defun proof-goto-command-end () - "Set point to end of command at point." - (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))))) - (proof-assert-next-command nil - 'ignore-proof-process - 'dontmoveforward)) - (skip-chars-backward " \t\n") - (backward-char))) ; should land on terminal char - - - -;; -;; Mouse functions -;; - -;; FIXME oddity here: with proof-follow-mode='locked, when retracting, -;; point stays where clicked. When advancing, it moves. Might -;; be nicer behaviour than actually moving point into locked region -;; which is only useful for cut and paste, really. -(defun proof-mouse-goto-point (event) - "Call proof-goto-point on the click position." - (interactive "e") - (proof-maybe-save-point - (mouse-set-point event) - (proof-goto-point))) - - -;; FIXME da: this is an oddity. It copies the span, but does not -;; send it, contrary to it's old name ("proof-send-span"). -;; Now made more general to behave like mouse-track-insert -;; when not over a span. -;; FIXME da: improvement would be to allow selection of part -;; of command by dragging, as in ordinary mouse-track-insert. -;; Maybe by setting some of the mouse track hooks. -(defun proof-mouse-track-insert (event) - "Copy highlighted command under the mouse to point. Ignore comments. -If there is no command under the mouse, behaves like mouse-track-insert." - (interactive "e") - (let ((str - (save-window-excursion - (save-excursion - (let* ((span (span-at (mouse-set-point event) 'type))) - (and - span - ;; Next test might be omitted to allow for non-script - ;; buffer copying (e.g. from spans in the goals buffer) - (eq (current-buffer) proof-script-buffer) - ;; Test for type=vanilla means that closed goal-save regions - ;; are not copied. - (eq (span-property span 'type) 'vanilla) - ;; Finally, extracting the 'cmd part prevents copying - ;; comments, and supresses leading spaces, at least. - ;; Odd. - (span-property span 'cmd))))))) - ;; Insert copied command in original window, - ;; buffer, point position. - (if str - (insert str proof-script-command-separator) - (mouse-track-insert event)))) - - - - +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Restarting and clearing spans (FIXME: belongs in core code, above) ;; @@ -2262,413 +2032,6 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}." (delete-spans (proof-locked-end) (point-max) 'type)))) -;; -;; Minibuffer non-scripting command -;; - -(defvar proof-minibuffer-history nil - "History of proof commands read from the minibuffer") - -(defun proof-minibuffer-cmd (cmd) - "Prompt for a command in the minibuffer and send it to proof assistant. -The command isn't added to the locked region. - -If a prefix arg is given and there is a selected region, that is -pasted into the command. This is handy for copying terms, etc from -the script. - -If `proof-strict-state-preserving' is set, and `proof-state-preserving-p' -is configured, then the latter is used as a check that the command -will be safe to execute, in other words, that it won't ruin -synchronization. If when applied to the command it returns false, -then an error message is given. - -WARNING: this command risks spoiling synchronization if the test -`proof-state-preserving-p' is not configured, if it is -only an approximate test, or if `proof-strict-state-preserving' -is off (nil)." - (interactive - (list (read-string "Command: " - (if (and current-prefix-arg (region-exists-p)) - (replace-in-string - (buffer-substring (region-beginning) (region-end)) - "[ \t\n]+" " ")) - 'proof-minibuffer-history))) - (if (and proof-strict-state-preserving - proof-state-preserving-p - (not (funcall proof-state-preserving-p cmd))) - (error "Command is not state preserving, I won't execute it!")) - (proof-shell-invisible-command cmd)) - - -;; -;; Frobbing locked end -;; - -;; 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. - -;; In fact, it's so risky, we'll disable it by default -(if (if proof-running-on-XEmacs - (get 'proof-frob-locked-end 'disabled t) - ;; FSF code more approximate - (not (member 'disabled (symbol-plist 'proof-frob-locked-end)))) - (put 'proof-frob-locked-end 'disabled t)) - -(defun proof-frob-locked-end () - "Move the end of the locked region backwards to regain synchronization. -Only for use by consenting adults. - -This command can be used to repair synchronization in case something -goes wrong and you want to tell Proof General that the proof assistant -has processed less of your script than Proof General thinks. - -You should only use it to move the locked region to the end of -a proof command." - (interactive) - (cond - (proof-shell-busy - (error "You can't use this command while %s is busy!" proof-assistant)) - ((not (eq (current-buffer) proof-script-buffer)) - (error "Must be in the active scripting buffer.")) - ;; Sometimes may need to move point forwards, when locked region - ;; is editable. - ;; ((> (point) (proof-locked-end)) - ;; (error "You can only move point backwards.")) - ;; FIXME da: should move to a command boundary, really! - (t (proof-set-locked-end (point)) - (delete-spans (proof-locked-end) (point-max) 'type)))) - - - - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; command history (unfinished) -;; -;; da: below functions for input history simulation are quick hacks. -;; Could certainly be made more efficient. - -;(defvar proof-command-history nil -; "History used by proof-previous-matching-command and friends.") - -;(defun proof-build-command-history () -; "Construct proof-command-history from script buffer. -;Based on position of point." -; ;; let -; ) - -;(defun proof-previous-matching-command (arg) -; "Search through previous commands for new command matching current input." -; (interactive)) -; ;;(if (not (memq last-command '(proof-previous-matching-command -; ;; proof-next-matching-command))) -; ;; Start a new search - -;(defun proof-next-matching-command (arg) -; "Search through following commands for new command matching current input." -; (interactive "p") -; (proof-previous-matching-command (- arg))) - -;; -;; end command history stuff -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; -;;; Non-scripting proof assistant commands. -;;; - -;;; These are based on defcustom'd settings so that users may -;;; re-configure the system to their liking. - - -;; FIXME: da: add more general function for inserting into the -;; script buffer and the proof process together, and using -;; a choice of minibuffer prompting (hated by power users, perfect -;; for novices). -;; TODO: -;; Add named goals. -;; Coherent policy for movement here and elsewhere based on -;; proof-one-command-per-line user option. -;; Coherent policy for sending to process after writing into -;; script buffer. Could have one without the other. -;; For example, may be more easy to edit complex goal string -;; first in the script buffer. Ditto for tactics, etc. - - - -;; -;; Helper macros and functions -;; - -;; See put expression at end to give this indentation like while form -(defmacro proof-if-setting-configured (var &rest body) - "Give error if a configuration setting VAR is unset, otherwise eval BODY." - `(if ,var - (progn ,@body) - (error "Proof General not configured for this: set %s" - ,(symbol-name var)))) - -(defmacro proof-define-assistant-command (fn doc cmdvar &optional body) - "Define command FN to send string BODY to proof assistant, based on CMDVAR. -BODY defaults to CMDVAR, a variable." - `(defun ,fn () - ,(concat doc - (concat "\nIssues a command to the assistant based on " - (symbol-name cmdvar) ".") - "") - (interactive) - (proof-if-setting-configured ,cmdvar - (proof-shell-invisible-command ,(or body cmdvar))))) - -(defmacro proof-define-assistant-command-witharg (fn doc cmdvar prompt &rest body) - "Define command FN to prompt for string CMDVAR to proof assistant. -CMDVAR is a function or string. Automatically has history." - `(progn - (defvar ,(intern (concat (symbol-name fn) "-history")) nil - ,(concat "History of arguments for " (symbol-name fn) ".")) - (defun ,fn (arg) - ,(concat doc "\nIssues a command based on ARG to the assistant, using " - (symbol-name cmdvar) ".\n" - "The user is prompted for an argument.") - (interactive - (proof-if-setting-configured ,cmdvar - (if (stringp ,cmdvar) - (list (format ,cmdvar - (read-string - ,(concat prompt ": ") "" - ,(intern (concat (symbol-name fn) "-history"))))) - (funcall ,cmdvar)))) - ,@body))) - -(defun proof-issue-new-command (cmd) - "Insert CMD into the script buffer and issue it to the proof assistant. -If point is in the locked region, move to the end of it first. -Start up the proof assistant if necessary." - (proof-with-script-buffer - (if (proof-shell-live-buffer) - (if (proof-in-locked-region-p) - (proof-goto-end-of-locked t))) - (proof-script-new-command-advance) - ;; FIXME: fixup behaviour of undo here. Really want to temporarily - ;; disable undo for insertion. but (buffer-disable-undo) trashes - ;; whole undo list! - (insert cmd) - ;; FIXME: could do proof-indent-line here, but let's wait until - ;; indentation is fixed. - (proof-assert-until-point-interactive))) - -;; -;; Commands which do not require a prompt and send an invisible -;; command. -;; - -(proof-define-assistant-command proof-prf - "Show the current proof state." - proof-showproof-command) -(proof-define-assistant-command proof-ctxt - "Show the current context." - proof-context-command) -(proof-define-assistant-command proof-help - "Show a help or information message from the proof assistant. -Typically, a list of syntax of commands available." - proof-info-command) -(proof-define-assistant-command proof-cd - "Change directory to the default directory for the current buffer." - proof-shell-cd-cmd - (proof-format-filename proof-shell-cd-cmd - ;; FSF fix: use default-directory rather than fn - default-directory)) - -(defun proof-cd-sync () - "If proof-shell-cd-cmd is set, do proof-cd and wait for prover ready. -This is intended as a value for proof-activate-scripting-hook" - ;; The hook is set in proof-mode before proof-shell-cd-cmd may be set, - ;; so we explicitly test it here. - (if proof-shell-cd-cmd - (progn - (proof-cd) - (proof-shell-wait)))) - -;; -;; Commands which require an argument, and maybe affect the script. -;; - -;; FIXME: maybe move these to proof-menu - -(proof-define-assistant-command-witharg proof-find-theorems - "Search for items containing given constants." - proof-find-theorems-command - "Find theorems containing" - (proof-shell-invisible-command arg)) - -(proof-define-assistant-command-witharg proof-issue-goal - "Write a goal command in the script, prompting for the goal." - proof-goal-command - "Goal" - (let ((proof-one-command-per-line t)) ; Goals always start at a new line - (proof-issue-new-command arg))) - -(proof-define-assistant-command-witharg proof-issue-save - "Write a save/qed command in the script, prompting for the theorem name." - proof-save-command - "Save as" - (let ((proof-one-command-per-line t)) ; Saves always start at a new line - (proof-issue-new-command arg))) - - - - - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; Electric terminator mode -;; -;; NB: only relevant for provers with a "terminal char" which -;; terminates commands in proof scripts. - -;; Register proof-electric-terminator as a minor mode. - -(deflocal proof-electric-terminator nil - "Fake minor mode for electric terminator.") - -(or (assq 'proof-electric-terminator minor-mode-alist) - (setq minor-mode-alist - (append minor-mode-alist - (list '(proof-electric-terminator - (concat " " proof-terminal-string)))))) - -;; This is a value used by custom-set property = proof-set-value. -(defun proof-electric-terminator-enable () - "Copy proof-electric-terminator-enable to all script mode copies of it. -Make sure the modeline is updated to display new value for electric terminator." - (if proof-mode-for-script - (proof-map-buffers (proof-buffers-in-mode proof-mode-for-script) - (setq proof-electric-terminator - proof-electric-terminator-enable))) - (redraw-modeline)) - -(proof-deftoggle proof-electric-terminator-enable proof-electric-terminator-toggle) - -(defun proof-electric-term-incomment-fn () - "Used as argument to proof-assert-until-point." - ;; CAREFUL: (1) dynamic scoping here - ;; (2) needs this name to be recognized in - ;; proof-assert-until-point - (setq incomment t) - (if ins (backward-delete-char 1)) - (goto-char mrk) - (insert proof-terminal-string)) - -;; FIXME da: this function is a mess and needs rewriting. -;; (proof-assert-until-point process needs cleaning up) -;; -;; What it should do: -;; * parse FIRST. If we're inside a comment or string, -;; then insert the terminator where we are. Otherwise -;; can skip backwards and insert the terminator at the -;; command end (perhaps optionally), and look for -;; existing terminator. - -(defun proof-process-electric-terminator () - "Insert the proof command terminator, and assert up to it. -This is a little bit clever with placement of semicolons, and will -try to avoid duplicating them in the buffer. -When used in the locked region (and so with strict read only off), it -always defaults to inserting a semi (nicer might be to parse for a -comment, and insert or skip to the next semi)." - (let ((mrk (point)) ins incomment) - (if (< mrk (proof-locked-end)) - ;; In locked region, just insert terminator without further ado - (insert proof-terminal-char) - ;; Otherwise, do other thing. - ;; Old idea: only shift terminator wildly if we're looking at - ;; whitespace. Why? - ;; (if (looking-at "\\s-\\|\\'\\|\\w") - (if (proof-only-whitespace-to-locked-region-p) - (error "There's nothing to do!")) - - (if (not (= (char-after (point)) proof-terminal-char)) - (progn - (forward-char) ;; immediately after command end. - (insert proof-terminal-string) - (setq ins t))) - (proof-assert-until-point 'proof-electric-term-incomment-fn) - (or incomment - (proof-script-next-command-advance))))) - -(defun proof-electric-terminator () - "Insert the terminator, perhaps sending the command to the assistant. -If proof-electric-terminator-enable is non-nil, the command will be -sent to the assistant." - (interactive) - (if proof-electric-terminator-enable - (proof-process-electric-terminator) - (self-insert-command 1))) - - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; Completion based on <PA>-completion-table -;; -;; Requires completion.el package. Completion is usually -;; a hand-wavy thing, so we don't make any attempt to maintain -;; a precise completion table or anything. -;; -;; New in 3.2. -;; -(defun proof-add-completions () - "Add completions from <PA>-completion-table to completion database. -Uses `add-completion' with a negative number of uses and ancient -last use time, to discourage saving these into the users database." - (interactive) - (require 'completion) - (mapcar (lambda (cmpl) - ;; completion gives error in this case; trapping - ;; the error here is tricky in FSF Emacs so duplicate - ;; the test. - (if (>= (length cmpl) completion-min-length) - (add-completion cmpl -1000 0))) - (proof-ass completion-table))) - -;; NB: completion table is expected to be set when proof-script -;; is loaded! Can call proof-script-add-completions if the table -;; is updated. -(eval-after-load "completion" - '(proof-add-completions)) - -(defun proof-script-complete (&optional arg) - "Like `complete' but case-fold-search set to proof-case-fold-search." - (interactive "*p") - (let ((case-fold-search proof-case-fold-search)) - (complete arg))) - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; Tags table building -;; -;; New in 3.2... or perhaps later. -;; -;; FIXME: incomplete. Add function to build tags table from -;; - - - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |