diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 22 | ||||
| -rw-r--r-- | generic/proof-script.el | 49 | ||||
| -rw-r--r-- | generic/proof-shell.el | 12 | ||||
| -rw-r--r-- | generic/proof-site.el | 4 | ||||
| -rw-r--r-- | generic/proof-toolbar.el | 7 | ||||
| -rw-r--r-- | generic/span-overlay.el | 2 |
6 files changed, 66 insertions, 30 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 31586553..befd32c0 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -103,7 +103,10 @@ use because of a bug." (defcustom proof-strict-read-only ;; For FSF Emacs, strict read only is buggy when used in ;; conjunction with font-lock. - (string-match "XEmacs" emacs-version) + + ;; The second conjunctive ensures that the expression is either + ;; `nil' or `strict' (and not 15). + (and (string-match "XEmacs" emacs-version) 'strict) "*Whether Proof General is strict about the read-only region in buffers. If non-nil, an error is given when an attempt is made to edit the read-only region. If nil, Proof General is more relaxed (but may give @@ -335,6 +338,7 @@ Suggestion: this can be set in the shell mode configuration." :type 'function :group 'prover-config) +;; FIXME: ought to be renamed to proof-mode-for-goals (defcustom proof-mode-for-pbp 'pbp-mode "Mode for proof state display buffers. Usually customised for specific prover. @@ -412,7 +416,7 @@ insert when called interactively." (defcustom proof-terminal-char nil - "Character which terminates a proof command in a script buffer." + "Character which terminates a command in a script buffer." :type 'character :group 'proof-script) @@ -423,7 +427,7 @@ The script buffer's comment-start is set to this string plus a space." :group 'proof-script) (defcustom proof-comment-end "" - "String which starts a comment in the proof assistant command language. + "String which ends a comment in the proof assistant command language. The script buffer's comment-end is set to this string plus a space." :type 'string :group 'proof-script) @@ -572,7 +576,7 @@ The special string proof-no-command means there is nothing to do." "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" +when parsing the proofstate output." :type 'function :group 'proof-script) @@ -588,7 +592,7 @@ This is used to handle nested goals allowed by some provers." :group 'proof-script) (defcustom proof-state-preserving-p nil - "A predicate, non-nil if its argument preserves the proof state." + "A predicate, non-nil if its argument (a command) preserves the proof state." :type 'function :group 'proof-script) @@ -689,7 +693,7 @@ group. This allows different proof assistants to coexist ;; (defcustom proof-shell-prompt-pattern nil - "Proof shell's value for comint-prompt-pattern, which see." + "Proof shell's value for comint-prompt-pattern." :type 'regexp :group 'proof-shell) @@ -736,7 +740,7 @@ otherwise it will be lost." (defcustom proof-shell-interrupt-regexp nil "Regexp matching output indicating the assistant was interrupted. -Similar notes apply as for proof-shell-error-regexp, which see." +Similar notes apply as for `proof-shell-error-regexp'." :type 'regexp :group 'proof-shell) @@ -1026,7 +1030,7 @@ inserted." (defcustom proof-splash-extensions nil "Prover specific extensions of splash screen. -These are evaluated and appended to proof-splash-contents, which see." +These are evaluated and appended to `proof-splash-contents'." :type 'sexp :group 'proof-config) @@ -1055,7 +1059,7 @@ These are evaluated and appended to proof-splash-contents, which see." (defcustom proof-universal-keys '(([(control c) (control c)] . proof-interrupt-process) ([(control c) (control v)] . proof-execute-minibuffer-cmd)) -"List of keybindings made for both the script and response buffer. +"List of keybindings made for the script, goals and response buffer. Elements of the list are tuples `(k . f)' where `k' is a keybinding (vector) and `f' the designated function." :type 'sexp diff --git a/generic/proof-script.el b/generic/proof-script.el index 06c768ae..d9d5c686 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -873,6 +873,13 @@ Assumes that point is at the end of a command." (forward-line))) +(defun proof-assert-until-point-interactive () + "Process the region from the end of the locked-region until point. +Default action if inside a comment is just process as far as the start of +the comment." + (interactive) + (proof-assert-until-point)) + ; Assert until point - We actually use this to implement the ; assert-until-point, active terminator keypress, and find-next-terminator. @@ -889,11 +896,12 @@ Assumes that point is at the end of a command." (&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 process as far as the start of -the comment. If you want something different, put it inside +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 and the buffer will not be activated for scripting." - (interactive) (unless ignore-proof-process-p (proof-shell-ready-prover) (proof-activate-scripting)) @@ -930,17 +938,23 @@ scripting." ;; FIXME: polish the undo behaviour and quit behaviour of this ;; command (should inhibit quit somewhere or other). +(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-assert-next-command)) + (defun proof-assert-next-command (&optional unclosed-comment-fun ignore-proof-process-p dont-move-forward for-new-command) "Process until the end of the next unprocessed command after point. If inside a comment, just process 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. Afterwards, move forward to near the next command afterwards, unless DONT-MOVE-FORWARD is non-nil. If FOR-NEW-COMMAND is non-nil, a space or newline will be inserted automatically." - (interactive) (unless ignore-proof-process-p (proof-shell-ready-prover) ;; FIXME: check this @@ -1073,6 +1087,13 @@ deletes the region corresponding to the proof sequence." ;; FIXME da: Maybe retraction to the start of ;; a file should remove it from the list of included files? +(defun proof-retract-until-point-interactive () + "Tell the proof process to retract until point. +If invoked outside a locked region, undo the last successfully processed +command." + (interactive) + (proof-retract-until-point)) + (defun proof-retract-until-point (&optional delete-region) "Set up the proof process for retracting until point. In particular, set a flag for the filter process to call @@ -1082,7 +1103,6 @@ If DELETE-REGION is non-nil, delete the region in the proof script corresponding to the proof command sequence. If invoked outside a locked region, undo the last successfully processed command." - (interactive) (proof-shell-ready-prover) (proof-activate-scripting) (let ((span (span-at (point) 'type))) @@ -1150,12 +1170,16 @@ UNCLOSED-COMMENT-FUN." ;; misc other user functions ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +(defun proof-undo-last-successful-command-interactive () + "Undo last successful command at end of locked region. +The text is also deleted from the proof script." + (interactive "p") + (proof-undo-last-successful-command)) (defun proof-undo-last-successful-command (&optional no-delete) "Undo last successful command at end of locked region. Unless optional NO-DELETE is set, the text is also deleted from the proof script." - (interactive "p") (unless (proof-locked-region-empty-p) (let ((lastspan (span-at-before (proof-locked-end) 'type))) (if lastspan @@ -1208,7 +1232,7 @@ the proof script." "Process the current buffer and set point at the end of the buffer." (interactive) (goto-char (point-max)) - (proof-assert-until-point)) + (proof-assert-until-point-interactive)) ;; FIXME da: this could do with some tweaking. Be careful to ;; avoid memory leaks. If a buffer is killed and it's local @@ -1433,7 +1457,7 @@ Start up the proof assistant if necessary." (insert cmd) ;; FIXME: could do proof-indent-line here, but let's ;; wait until indentation is fixed. - (proof-assert-until-point)) + (proof-assert-until-point-interactive)) @@ -1540,8 +1564,7 @@ No action if BUF is nil." 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." +If active terminator mode is enabled, pressing a terminator will automatically activate `proof-assert-next-command' for convenience." (interactive "P") @@ -1635,11 +1658,11 @@ Otherwise just do proof-restart-buffers to delete some spans from memory." (let ((map proof-mode-map)) (define-key map [(control c) (control e)] 'proof-find-next-terminator) (define-key map [(control c) (control a)] 'proof-goto-command-start) -(define-key map [(control c) (control n)] 'proof-assert-next-command) -(define-key map [(control c) (return)] 'proof-assert-next-command) +(define-key map [(control c) (control n)] 'proof-assert-next-command-interactive) +(define-key map [(control c) (return)] 'proof-assert-next-command-interactive) (define-key map [(control c) (control t)] 'proof-try-command) -(define-key map [(control c) ?u] 'proof-retract-until-point) -(define-key map [(control c) (control u)] 'proof-undo-last-successful-command) +(define-key map [(control c) ?u] 'proof-retract-until-point-interactive) +(define-key map [(control c) (control u)] 'proof-undo-last-successful-command-interactive) (define-key map [(control c) ?\'] 'proof-goto-end-of-locked-interactive) ;; FIXME da: I don't understand what this function is supposed to do. ;; It will copy a proof command from within the locked region diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 7bb5c6e0..83098f88 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -66,9 +66,14 @@ Set in proof-shell-mode.") (SPAN,COMMAND,ACTION) triples, which is a queue of things to do. -See the functions proof-start-queue and proof-exec-loop.") +See the functions `proof-start-queue' and `proof-exec-loop'.") +(defvar proof-analyse-using-stack nil + "Choice of syntax tree encoding for terms. +If `nil', prover is expected to make no optimisations. +If non-`nil', the pretty printer of the prover only reports local changes. +For LEGO 1.3.1 use `nil', for Coq 6.2, use `t'.") ;; @@ -362,7 +367,7 @@ left around so the user may discover what killed the process." "Clear script buffers and send proof-shell-restart-cmd. All locked regions are cleared and the active scripting buffer deactivated. The restart command should re-synchronize -Proof General with the proof assitant." +Proof General with the proof assistant." (interactive) (proof-script-remove-all-spans-and-deactivate) (setq proof-included-files-list nil @@ -1390,7 +1395,6 @@ before and after sending the command." ;; Proof General shell mode definition ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; OLD COMMENT: "This has to come after proof-mode is defined" ;;###autoload (eval-and-compile ; to define vars @@ -1440,7 +1444,7 @@ before and after sending the command." ;; watch difference with proof-shell-menu, proof-shell-mode-menu. (defvar proof-shell-menu proof-shared-menu - "The menu for the Proof-assistant shell") + "The menu for the Proof-assistant shell.") (easy-menu-define proof-shell-mode-menu proof-shell-mode-map diff --git a/generic/proof-site.el b/generic/proof-site.el index e758bf60..91802d1f 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -103,7 +103,7 @@ You can use customize to set this variable." (mapcar (lambda (astnt) (car astnt)) proof-assistant-table) (concat - "*Choice of proof assitants to use with Proof General. + "*Choice of proof assistants to use with Proof General. A list of symbols chosen from:" (apply 'concat (mapcar (lambda (astnt) (concat " '" (symbol-name (car astnt)))) @@ -141,7 +141,7 @@ NOTE: to change proof assistant, you must start a new Emacs session.") ;; Now add auto-loads and load-path elements to support the ;; proof assistants selected, and define a stub -(let ((assistants proof-assistants) assistant) +(let ((assistants proof-assistants)) (while assistants (let* ((assistant (car assistants)) ; compiler bogus warning here diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index a89dc536..4a0c3e68 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -13,8 +13,11 @@ ;; Toolbar is just for scripting buffer at the moment. ;; + +;;; IMPORT declaration (require 'proof-script) (autoload 'proof-shell-live-buffer "proof-shell") +(autoload 'proof-shell-restart "proof-shell") (defconst proof-toolbar-default-button-list '(proof-toolbar-goal-button @@ -302,7 +305,7 @@ Move point if the end of the locked position is invisible." (progn (proof-toolbar-move (goto-char (proof-unprocessed-begin)) - (proof-assert-next-command)) + (proof-assert-next-command-interactive)) (proof-toolbar-follow)))) @@ -321,7 +324,7 @@ Move point if the end of the locked position is invisible." (progn (proof-toolbar-move (goto-char (point-min)) - (proof-retract-until-point)) ; gives error if process busy + (proof-retract-until-point-interactive)) ; gives error if process busy (proof-toolbar-follow)) (error "Nothing to retract in this buffer!"))) diff --git a/generic/span-overlay.el b/generic/span-overlay.el index fa113911..6cb572df 100644 --- a/generic/span-overlay.el +++ b/generic/span-overlay.el @@ -67,6 +67,8 @@ elements = S0 S1 S2 .... [tl-seq.el]" (defun span-read-only-hook (overlay after start end &optional len) (error "Region is read-only")) +;;; FIXME: This is too harsh and breaks font-lock +;;; If only faces are modified we shouldn't call span-read-only-hook (defun span-read-only (span) "Set SPAN to be read only." ;; Unfortunately, this function is called on spans which are |