diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-abbrev.el | 37 | ||||
| -rw-r--r-- | coq/coq.el | 144 |
2 files changed, 129 insertions, 52 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 8db7781e..e88f9ca8 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -113,22 +113,6 @@ :selected (eq proof-three-window-mode-policy 'vertical) :help "One column mode"]) ["Refresh Windows Layout" proof-layout-windows t] - ("Automatic Proof using annotations..." - ["ask" - (customize-set-variable 'coq-accept-proof-using-suggestion 'ask) - :style radio - :selected (eq coq-accept-proof-using-suggestion 'ask) - :help "ask user when a new proof using annotation is suggested"] - ["always" - (customize-set-variable 'coq-accept-proof-using-suggestion 'always) - :style radio - :selected (eq coq-accept-proof-using-suggestion 'always) - :help "Always update the proof using annotation when suggested"] - ["never" - (customize-set-variable 'coq-accept-proof-using-suggestion 'never) - :style radio - :selected (eq coq-accept-proof-using-suggestion 'never) - :help "never update the proof using"]) ["Toggle tooltips" proof-output-tooltips-toggle :style toggle :selected proof-output-tooltips @@ -252,6 +236,27 @@ :style radio :selected (eq coq-diffs 'removed) :help "Show diffs: added and removed"]) + ("\"Proof using\" mode..." + ["ask" + (customize-set-variable 'coq-accept-proof-using-suggestion 'ask) + :style radio + :selected (eq coq-accept-proof-using-suggestion 'ask) + :help "Ask user when a new proof using annotation is suggested"] + ["always" + (customize-set-variable 'coq-accept-proof-using-suggestion 'always) + :style radio + :selected (eq coq-accept-proof-using-suggestion 'always) + :help "Always update the proof using annotation when suggested"] + ["highlight" + (customize-set-variable 'coq-accept-proof-using-suggestion 'highlight) + :style radio + :selected (eq coq-accept-proof-using-suggestion 'highlight) + :help "Highight the proof when an auto insert is suggested (right click to insert))"] + ["Ignore" + (customize-set-variable 'coq-accept-proof-using-suggestion 'ignore) + :style radio + :selected (eq coq-accept-proof-using-suggestion 'ignore) + :help "no highlight (right click insertion still possible)"]) "" ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"] ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"] @@ -109,7 +109,9 @@ Namely, goals that do not fit in the goals window." ;TODO: remove Set Undo xx. It is obsolete since coq-8.5 at least. ;;`(,(format "Set Undo %s . " coq-default-undo-limit) "Set Printing Width 75.") (defconst coq-shell-init-cmd - (append `(,(format "Add Search Blacklist %s. " coq-search-blacklist-string)) coq-user-init-cmd) + (append `(,(format "Add Search Blacklist %s. " coq-search-blacklist-string)) + '("Set Suggest Proof Using. ") + coq-user-init-cmd) "Command to initialize the Coq Proof Assistant.") @@ -1972,6 +1974,8 @@ at `proof-assistant-settings-cmds' evaluation time.") proof-no-fully-processed-buffer t + proof-dependency-menu-system-specific coq-dependency-menu-system-specific + proof-dependencies-system-specific coq-dependencies-system-specific ;; Coq has no global settings? ;; (proof-assistant-settings-cmd) @@ -2564,52 +2568,120 @@ Warning: this makes the error messages (and location) wrong.") ;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;; (setq coq-shell-theorem-dependency-list-regexp - "<infomsg>\\(?: \\|\n\\)The proof of \\([^ \n]+\\)\\(?: \\|\n\\)should start with one of the following commands:\\(?: \\|\n\\)Proof using\\([^.]*\\)\\.") - -(defcustom accept-proof-using-suggestion 'ask - "Wether proofgeneral should automatically update proof using when -recieving suggestions from coq at Qed time." + "<infomsg>\n?The proof of \\([^ \n]+\\)\\(?: \\|\n\\)should start with one of the following commands:\\(?: \\|\n\\)Proof using\\([^.]*\\)\\.") + +(defcustom coq-accept-proof-using-suggestion 'highlight + "Wether and how proofgeneral should insert \"Proof using\" suggestions. +Suggestions are emitted by Coq at Qed time. The possible values +of this variable are: + +- 'always: always insert the suggested annotation + +- 'highlight (default value): highlight the Proof command and + have a contextual menu for insertion (or M-x + coq-insert-suggested-dependency when point is on the proof + considered) + +- 'ask: asks the user each time. If yes then do as 'always, else + do as 'highlight + +- 'never: ignore completely the suggestions. + +Remarks and limitations: +- do not support nested proofs. +- always use the *first* annotation suggested by coq. +- the proof is not replayed, which is consistent with the fact + that pg currently do not deal with async proofs. +- if there is already a \"Proof using\" annotation, then either it + is correct and nothing happens, or it is incorrect and coq + generates an error. PG won't try to replace the erroneous + annotation in this case, but you can always go back, remove it + by hand, and let pg insert the good one. +- instead of the menu you can do M-x coq-insert-suggested-dependency + when point is on the proof considered. +" :type '(choice (const :tag "Ask user" ask) - (const :tag "always accept" always) - (const :tag "never accept" never)) + (const :tag "Always accept" always) + (const :tag "Higihlight" never) + (const :tag "Ignore completely" ignore)) :group 'coq) -(defun coq-extract-proof-using-from-suggestion (span) - (let ((sp (span-property-safe span 'dependencies))) - sp)) - -(defun coq-insert-proof-using-suggestion (span suggested) +;; the additional menu for "proof using". highlights the "Proof." command, and +;; have a entry to insert the annotation and remove the highlight. +(defvar coq-dependency-menu-system-specific + (lambda (span) + (let* ((deps (span-property-safe span 'dependencies)) + (specialspans (spans-at-region-prop (span-start span) (span-end span) 'proofusing)) + (specialspan (and specialspans (not (cdr specialspans)) (car specialspans))) + (name (concat " insert \"proof using " (mapconcat 'identity deps " ") "\"")) + (fn `(lambda (sp) + (coq-insert-proof-using-suggestion sp t) + (span-delete ,specialspan)))) + (list "-------------" (vector name `(,fn ,span) (not (not deps)))))) + "Coq specific additional menu entry for \"Proof using\". +annotation. See `proof-dependency-menu-system-specific'." ) + +(defun coq-mark-span-dependencies (span suggested) + (goto-char (span-start span)) + (let* ((endpos (re-search-forward "\\<Proof\\(?:\\s-+using\\)?\\>\\([^.]*\\)\\.")) + (proof-pos (match-beginning 0)) + (newspan (span-make proof-pos endpos))) + (span-set-property newspan 'face 'proof-warning-face) + (span-set-property newspan 'help-echo "Right click to insert \"proof using\"") + (span-set-property newspan 'proofusing t))) + +(defun coq-insert-proof-using (proof-pos previous-content string-suggested) + (goto-char (+ 5 proof-pos)) ; "Proof" has length 6 + (let ((spl proof-locked-span)) + (span-read-write spl) ; temporarily make the locked span writable + (when previous-content (delete-char (length previous-content))) + (insert (concat " using " string-suggested)) + (proof-span-read-only spl))) + +(defun coq-insert-suggested-dependency () + (interactive) + (let* ((span (span-at (point) 'type)) + (deps (span-property-safe span 'dependencies)) + (specialspans (spans-at-region-prop (span-start span) (span-end span) 'proofusing)) + (specialspan (and specialspans (not (cdr specialspans)) (car specialspans)))) + (coq-insert-proof-using-suggestion span t) + (span-delete specialspan))) + +;; TODO: have 'ignoe option to completely ignore (not highlight) +;; and have 'never renamed into 'highlight +(defun coq-insert-proof-using-suggestion (span &optional force) "Add the proof using annotation, respecting `coq-accept-proof-using-suggestion'. Insert \" using xxx\" After the \"Proof\" of SPAN, where xxx is built from the list of strings in SUGGESTED." (with-current-buffer proof-script-buffer (save-excursion (goto-char (span-start span)) - (let* ((pos-unproc (point)) - (endpos (save-excursion - (search-forward-regexp "\\<Proof\\(?:\\s-+using\\)?\\>\\([^.]*\\)\\."))) - (proof-pos (and endpos (match-beginning 0))) - (previous-content (and endpos (split-string (match-string 1)))) - (string-suggested (mapconcat 'identity suggested " ")) - (same (and endpos (not (cl-set-exclusive-or previous-content suggested :test 'string-equal))))) - (when (and endpos (not same) - (or (equal coq-accept-proof-using-suggestion 'always) + (let* ((endpos (re-search-forward "\\<Proof\\(?:\\s-+using\\)?\\>\\([^.]*\\)\\."))) + (when endpos + (let* ((suggested (span-property span 'dependencies)) + (proof-pos (match-beginning 0)) + (previous-content (split-string (match-string 1))) + (string-suggested (mapconcat 'identity suggested " ")) + (same (and previous-content + (not (cl-set-exclusive-or previous-content suggested + :test 'string-equal)))) + (usersayyes + (and (not same) (not force) + (equal coq-accept-proof-using-suggestion 'ask) (y-or-n-p (concat "Update proof using annotation (" - string-suggested ")")))) - (goto-char (+ 5 proof-pos)) ; "Proof" has length 6 - ;(if (stored proof-strict-read-only) ) - (let ((spl proof-locked-span)) - ;; temporarily make the locked span writable - (span-read-write spl) - (delete-char (length previous-content)) - (insert (concat " using " string-suggested)) - ;; go back to `proof-strict-read-only' says - (proof-span-read-only spl))))))) - -(defun proof-dependencies-system-specific (name span) - (let ((suggested (coq-extract-proof-using-from-suggestion span))) - (coq-insert-proof-using-suggestion span suggested))) + string-suggested ")"))))) + (unless same + (if (or force (equal coq-accept-proof-using-suggestion 'always) usersayyes) + (coq-insert-proof-using proof-pos previous-content string-suggested) + (when (member coq-accept-proof-using-suggestion '(highlight ask)) + (coq-mark-span-dependencies span suggested) + (message "\"Proof using\" not set. M-x coq-insert-suggested-dependency or right click to add it. See also `coq-accept-proof-using-suggestion'.")))))))))) + +(defvar coq-dependencies-system-specific + (lambda (span) (coq-insert-proof-using-suggestion span)) + "Coq specific dependency mechanism. +Used for automatic insertion of \"Proof using\" annotations.") ;::::::::::::: inserting suggested Proof using XXX... ;;;;;;;;;; |