diff options
Diffstat (limited to 'coq/coq.el')
| -rw-r--r-- | coq/coq.el | 767 |
1 files changed, 619 insertions, 148 deletions
@@ -1,37 +1,48 @@ -;; coq.el --- Major mode for Coq proof assistant -*- coding: utf-8 -*- -;; Copyright (C) 1994-2009 LFCS Edinburgh. +;;; coq.el --- Major mode for Coq proof assistant -*- coding: utf-8 -*- + +;; This file is part of Proof General. + +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: Healfdene Goguen, Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> -;; -;; $Id$ +;; License: GPL (GNU GENERAL PUBLIC LICENSE) + +;;; Commentary: +;; +;;; Code: (eval-when-compile (require 'cl) (require 'proof-compat)) -(eval-when (compile) +(eval-when-compile (require 'proof-utils) (require 'span) (require 'outline) (require 'newcomment) (require 'etags) (unless (proof-try-require 'smie) - (defvar smie-indent-basic nil) - (defvar smie-rules-function nil)) - (defvar proof-info nil) ; dynamic scope in proof-tree-urgent-action - (defvar action nil) ; dynamic scope in coq-insert-as stuff - (defvar string nil) ; dynamic scope in coq-insert-as stuff - (defvar old-proof-marker nil) - ; dynamic scoq in coq-proof-tree-enable-evar-callback - (defvar coq-auto-insert-as nil) ; defpacustom - (defvar coq-time-commands nil) ; defpacustom - (defvar coq-use-project-file t) ; defpacustom - (defvar coq-use-editing-holes nil) ; defpacustom - (defvar coq-hide-additional-subgoals nil) ; defpacustom - (proof-ready-for-assistant 'coq)) ; compile for coq + (defvar smie-indent-basic) + (defvar smie-rules-function)) + (defvar proof-info) ; dynamic scope in proof-tree-urgent-action + (defvar action) ; dynamic scope in coq-insert-as stuff + (defvar string) ; dynamic scope in coq-insert-as stuff + (defvar old-proof-marker) + (defvar coq-keymap) + (defvar coq-one-command-per-line) + (defvar coq-auto-insert-as) ; defpacustom + (defvar coq-time-commands) ; defpacustom + (defvar coq-use-project-file) ; defpacustom + (defvar coq-use-editing-holes) ; defpacustom + (defvar coq-hide-additional-subgoals)) (require 'proof) (require 'coq-system) ; load path, option, project file etc. @@ -42,7 +53,6 @@ (require 'coq-seq-compile) ; sequential compilation of Requires (require 'coq-par-compile) ; parallel compilation of Requires - ;; for compilation in Emacs < 23.3 (NB: declare function only works at top level) (declare-function smie-bnf->prec2 "smie") (declare-function smie-rule-parent-p "smie") @@ -78,7 +88,7 @@ ;; :group 'coq) (defcustom coq-user-init-cmd nil - "user defined init commands for Coq. + "User defined init commands for Coq. These are appended at the end of `coq-shell-init-cmd'." :type '(repeat (cons (string :tag "command"))) :group 'coq) @@ -91,13 +101,13 @@ These are appended at the end of `coq-shell-init-cmd'." ;; Default coq is only Private_ and _subproof (defcustom coq-search-blacklist-string ; add this? \"_ind\" \"_rect\" \"_rec\" "\"Private_\" \"_subproof\"" - "String for blacklisting strings from requests to coq environment." + "String for blacklisting strings from requests to Coq environment." :type 'string :group 'coq) (defcustom coq-prefer-top-of-conclusion nil - "prefer start of the conclusion over its end when displaying goals -that do not fit in the goals window." + "Prefer start of the conclusion over its end when displaying large goals. +Namely, goals that do not fit in the goals window." :type 'boolean :group 'coq) @@ -146,7 +156,7 @@ that do not fit in the goals window." (defcustom coq-end-goals-regexp-show-subgoals "\n(dependent evars:" "Regexp for `proof-shell-end-goals-regexp' when showing all subgoals. -A setting of nil means show all output from Coq. See also +A setting of nil means show all output from Coq. See also option `coq-hide-additional-subgoals'." :type '(choice regexp (const nil)) :group 'coq) @@ -154,7 +164,7 @@ A setting of nil means show all output from Coq. See also (defcustom coq-end-goals-regexp-hide-subgoals (concat "\\(\nsubgoal 2 \\)\\|\\(" coq-end-goals-regexp-show-subgoals "\\)") "Regexp for `proof-shell-end-goals-regexp' when hiding additional subgoals. -See also `coq-hide-additional-subgoals'." +See also option `coq-hide-additional-subgoals'." :type '(choice regexp (const nil)) :group 'coq) @@ -306,32 +316,28 @@ See also `coq-hide-additional-subgoals'." ;; Derived modes ;; -(eval-and-compile ;; FIXME: Why? - (define-derived-mode coq-shell-mode proof-shell-mode - "Coq Shell" nil - (coq-shell-mode-config))) +(define-derived-mode coq-shell-mode proof-shell-mode + "Coq Shell" nil + (coq-shell-mode-config)) -(eval-and-compile ;; FIXME: Why? - (define-derived-mode coq-response-mode proof-response-mode +(define-derived-mode coq-response-mode proof-response-mode "Coq Response" nil - (coq-response-config))) + (coq-response-config)) -(eval-and-compile ;; FIXME: Why? - (define-derived-mode coq-mode proof-mode "Coq" - "Major mode for Coq scripts. +(define-derived-mode coq-mode proof-mode "Coq" + "Major mode for Coq scripts. \\{coq-mode-map}" - (coq-mode-config))) + (coq-mode-config)) -(eval-and-compile ;; FIXME: Why? - (define-derived-mode coq-goals-mode proof-goals-mode - "Coq Goals" nil - (coq-goals-mode-config))) +(define-derived-mode coq-goals-mode proof-goals-mode + "Coq Goals" nil + (coq-goals-mode-config)) ;; Indentation and navigation support via SMIE. (defcustom coq-use-smie t - "OBSOLETE. smie code is always used now. + "OBSOLETE. smie code is always used now. If non-nil, Coq mode will try to use SMIE for indentation. SMIE is a navigation and indentation framework available in Emacs >= 23.3." @@ -370,8 +376,8 @@ SMIE is a navigation and indentation framework available in Emacs >= 23.3." ;; would not be shown in response buffer. If it is before, then we want it ;; urgent so that it is displayed. (defvar coq-eager-no-urgent-regex "\\s-*Finished " - "Regexp of commands matching proof-shell-eager-annotation-start - that should maybe not be classified as urgent messages.") + "Regexp of commands matching ‘proof-shell-eager-annotation-start’ +that should maybe not be classified as urgent messages.") ;; return the end position if found, nil otherwise (defun coq-non-urgent-eager-annotation () @@ -436,7 +442,8 @@ This is a subroutine of `proof-shell-filter'." (set-marker proof-shell-urgent-message-scanner (if end ;; couldn't find message start; move forward to avoid rescanning - (max initstart + (max (or lastend 1) ;; goto after last end urgent msg + ;; or near the end of current output if that jumps farther. (- (point) (1+ proof-shell-eager-annotation-start-length))) ;; incomplete message; leave marker at start of message @@ -768,7 +775,7 @@ If locked span already has a state number, then do nothing. Also updates (defun coq-hide-additional-subgoals-switch () - "Function invoked when the user switches `coq-hide-additional-subgoals'." + "Function invoked when the user switches option `coq-hide-additional-subgoals'." (if coq-time-commands (progn (setq coq-hide-additional-subgoals nil) @@ -779,8 +786,8 @@ If locked span already has a state number, then do nothing. Also updates (setq proof-shell-end-goals-regexp coq-end-goals-regexp-show-subgoals)))) (defun coq-time-commands-switch () - "Function invoked when the user switches `coq-time-commands'. -Resets `coq-hide-additional-subgoals' and puts nil into + "Function invoked when the user switches option `coq-time-commands'. +Reset option `coq-hide-additional-subgoals' and puts nil into `proof-shell-end-goals-regexp' to ensure the timing is visible in the *goals* buffer." (if coq-time-commands @@ -799,7 +806,7 @@ the *goals* buffer." "Enumerates the different kinds of notation information one can ask to coq.") (defun coq-PrintScope () - "Show information on notations. Coq specific." + "Show information on notations. Coq specific." (interactive) (let* ((mods @@ -888,10 +895,10 @@ Support dot.notation.of.modules." (if notation (concat "\"" notation "\"") "")))) (defcustom coq-remap-mouse-1 nil - "Wether coq mode should remap mouse button 1 to coq queries. + "Whether Coq mode should remap mouse button 1 to Coq queries. This overrides the default global binding of (control mouse-1) and -(shift mouse-1) (buffers and faces menus). Hence it is nil by +\(shift mouse-1) (buffers and faces menus). Hence it is nil by default." :type 'boolean :group 'coq) @@ -939,13 +946,14 @@ Otherwise propose identifier at point if any." nil 'proof-minibuffer-history guess))) -(defun coq-ask-do (ask do &optional dontguess postformatcmd) +(defun coq-ask-do (ask do &optional dontguess postformatcmd wait) "Ask for an ident and print the corresponding term." (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd))) (proof-shell-ready-prover) (setq cmd (coq-guess-or-ask-for-string ask dontguess)) (proof-shell-invisible-command - (format (concat do " %s . ") (funcall postform cmd))))) + (format (concat do " %s . ") (funcall postform cmd)) + wait))) (defun coq-flag-is-on-p (testcmd) @@ -955,20 +963,29 @@ Otherwise propose identifier at point if any." (string-match "is on\\>" resp))) (defun coq-command-with-set-unset (setcmd cmd unsetcmd &optional postformatcmd testcmd) - "Play commands SETCMD then CMD and then silently UNSETCMD." + "Play commands SETCMD then CMD and then silently UNSETCMD. +The last UNSETCMD is performed with tag 'empty-action-list so that it +does not trigger ‘proof-shell-empty-action’ (which does \"Show\" at +the time of writing this documentation)." (let* ((postform (if (eq postformatcmd nil) 'identity postformatcmd)) (flag-is-on (and testcmd (coq-flag-is-on-p testcmd)))) + ;; We put 'empty-action-list tags on all three commands since we don't want + ;; to trigger "Show" or anything that we usually insert after a group of + ;; commands. (unless flag-is-on (proof-shell-invisible-command - (format " %s . " (funcall postform setcmd)) 'wait)) + (format " %s . " (funcall postform setcmd)) + nil nil 'no-response-display 'empty-action-list)) (proof-shell-invisible-command - (format " %s . " (funcall postform cmd)) 'wait) - (unless flag-is-on (proof-shell-invisible-command-invisible-result - (format " %s . " (funcall postform unsetcmd)))))) + (format " %s . " (funcall postform cmd)) 'wait nil 'empty-action-list) + (unless flag-is-on (proof-shell-invisible-command + (format " %s . " (funcall postform unsetcmd)) + 'waitforit nil 'no-response-display 'empty-action-list)))) (defun coq-ask-do-set-unset (ask do setcmd unsetcmd &optional dontguess postformatcmd tescmd) "Ask for an ident id and execute command DO in SETCMD mode. -More precisely it executes SETCMD, then DO id and finally silently UNSETCMD." +More precisely it executes SETCMD, then DO id and finally silently +UNSETCMD. See `coq-command-with-set-unset'." (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd tescmd))) (proof-shell-ready-prover) (setq cmd (coq-guess-or-ask-for-string ask dontguess)) @@ -1038,15 +1055,6 @@ This is specific to `coq-mode'." (interactive) (coq-ask-do "SearchRewrite" "SearchRewrite" nil)) -;; TODO SearchAbout become Search in v8.5, change when V8.4 becomes old. -(defun coq-SearchAbout () - (interactive) - (coq-ask-do - ;; TODO: use [Add Search Blacklist "foo"] to exclude optionaly some patterns: - ;; "_ind" "_rec" "R_" "_equation" - "SearchAbout (ex: \"eq_\" eq -bool)" - "SearchAbout") - (message "use [Coq/Settings/Search Blacklist] to change blacklisting.")) @@ -1058,6 +1066,11 @@ With flag Printing All if some prefix arg is given (C-u)." (coq-ask-do-show-all "Print" "Print") (coq-ask-do "Print" "Print"))) +(defun coq-Print-Ltac () + "Ask for an ident and print the corresponding Ltac term." + (interactive) + (coq-ask-do "Print Ltac" "Print Ltac")) + (defun coq-Print-with-implicits () "Ask for an ident and print the corresponding term." (interactive) @@ -1146,8 +1159,8 @@ With flag Printing All if some prefix arg is given (C-u)." (defun coq-get-response-string-at (&optional pt) "Go forward from PT until reaching a 'response property, and return it. Response span only starts at first non space character of a -command, so we may have to go forward to find it. Starts -from (point) if pt is nil. Precondition: pt (or point if nil) +command, so we may have to go forward to find it. Starts +from (point) if pt is nil. Precondition: pt (or point if nil) must be in locked region." (let ((pt (or pt (point)))) (save-excursion @@ -1158,10 +1171,10 @@ must be in locked region." (span-property (span-at (point) 'response) 'response)))) (defun coq-Show (withprintingall) - "Ask for a number i and show the ith goal. -Ask for a number i and show the ith current goal. With non-nil -prefix argument and not on the locked span, show the goal with -flag Printing All set." + "Ask for a number I and show the Ith goal. +Ask for a number I and show the ith current goal. With non-nil prefix +argument and not on the locked span, show the goal with flag +Printing All set." ; Disabled: ; "Ask for a number i and show the ith goal, or show ancient goal. ;If point is on a locked span, show the corresponding coq @@ -1198,8 +1211,8 @@ flag Printing All set." (coq-ask-do-show-all "Show goal number" "Show" t)) ;; Check -(eval-when (compile) - (defvar coq-auto-adapt-printing-width nil)); defpacustom +(eval-when-compile + (defvar coq-auto-adapt-printing-width)); defpacustom ;; Since Printing Width is a synchronized option in coq (?) it is retored ;; silently to a previous value when retracting. So we reset the stored width @@ -1209,8 +1222,8 @@ flag Printing All set." ;; FIXME: hopefully this will eventually become a non synchronized option and ;; we can remove this. (defun coq-set-auto-adapt-printing-width (&optional symb val); args are for :set compatibility - "Function called when setting `auto-adapt-printing-width'" - (setq symb val) + "Function called when setting `auto-adapt-printing-width'." + (setq symb val) ;; FIXME this is wrong (it should be 'set', but it would set nil sometimes) (if coq-auto-adapt-printing-width (progn (add-hook 'proof-assert-command-hook 'coq-adapt-printing-width) @@ -1222,14 +1235,37 @@ flag Printing All set." ;; of coq) Coq does not show the goals of enclosing proof when closing a nested ;; proof. This is coq's proof-shell-empty-action-list-command function which ;; inserts a "Show" if the last command of an action list is a save command and -;; there is more than one open proof before that save. +;; there is more than one open proof before that save. If you want to issue a +;; command and *not* have the goal redisplayed, the command must be tagged with +;; 'empty-action-list. (defun coq-empty-action-list-command (cmd) - (when (or (and (string-match coq-save-command-regexp-strict cmd) - (> (length coq-last-but-one-proofstack) 1)) - (and (string-match "\\(S\\|Uns\\)et\\s-+Printing" cmd) - (> (length coq-last-but-one-proofstack) 0))) - (list "Show."))) - + "Return the list of commands to send to Coq after CMD +if it is the last command of the action list. +If CMD is tagged with 'empty-action-list then this function won't +be called and no command will be sent to Coq." + (cond + ((or + ;; If closing a nested proof, Show the enclosing goal. + (and (string-match coq-save-command-regexp-strict cmd) + (> (length coq-last-but-one-proofstack) 1)) + ;; If user issued a printing option then t printing. + (and (string-match "\\(S\\|Uns\\)et\\s-+Printing" cmd) + (> (length coq-last-but-one-proofstack) 0))) + (list "Show.")) + ((or + ;; if we go back in the buffer and that the number of abort is less than + ;; the number of nested goals, then Unset Silent and Show the goal + (and (string-match "Backtrack\\s-+[[:digit:]]+\\s-+[[:digit:]]+\\(\\s-+[[:digit:]]*\\)" cmd) + (> (length (coq-get-span-proofstack (proof-last-locked-span))) + ;; the number of aborts is the third arg of Backtrack. + (string-to-number (match-string 1 cmd))))) + (list "Unset Silent." "Show.")) + ((or + ;; If we go back in the buffer and not in the above case, then only Unset + ;; silent (there is no goal to show). + (string-match "Backtrack" cmd)) + (list "Unset Silent.")))) + (defpacustom auto-adapt-printing-width t "If non-nil, adapt automatically printing width of goals window. Each timme the user sends abunch of commands to Coq, check if the @@ -1308,9 +1344,9 @@ present, current pg display mode and current geometry otherwise." ))) (defun coq-adapt-printing-width (&optional show width) - "Sends a Set Printing Width command to coq to fit the response window's width. -A Show command is also issued if SHOW is non-nil, so that the -goal is redisplayed." + "Sends a Set Printing Width command to Coq to fit the response window's WIDTH. +A Show command is also issued if SHOW is non-nil, so that the goal is +redisplayed." (interactive) (let ((wdth (or width (coq-guess-goal-buffer-at-next-command)))) ;; if no available width, or unchanged, do nothing @@ -1331,26 +1367,409 @@ goal is redisplayed." (rd (read-number (format "Width (%S): " deflt) deflt))) (coq-adapt-printing-width t rd))) +;;;;; utils fo overlays +(defun coq-overlays-at (pt prop) + (let ((overlays (overlays-at pt)) + found) + (while overlays + (let ((overlay (car overlays))) + (if (overlay-get overlay prop) + (setq found (cons overlay found)))) + (setq overlays (cdr overlays))) + found)) + +;;;;;;;;;; Hypothesis tracking ;;;;;;;;;; +;;; Facilities to build overlays for hyp names and hyp+type + hypcross +;;; ((un)folding buttons). +(defvar coq-hypname-map (make-sparse-keymap) "Keymap for visible hypothesis.") +(defvar coq-hypcross-map (make-sparse-keymap) "Keymap for visible hypothesis.") + +(defvar coq-hypcross-hovering-help t + "Whether hyps fold cross pops up a help when hovered.") + +(defvar coq-hyps-positions nil + "The list of positions of hypothesis in the goals buffer. +Maintained by a hook in `proof-shell-handle-delayed-output-hook'.") + +;; Hyps name are clickable and have a special keymap. +(defun coq-make-hypname-overlay (beg end h buf) + (let ((ov (make-overlay beg end buf))) + (when ov + (overlay-put ov 'evaporate t) + (overlay-put ov 'is-hypname t) + (overlay-put ov 'hyp-name h) + (overlay-put ov 'keymap coq-hypname-map)) + ov)) + +;; Hyps types are clickable only when folded +(defun coq-make-hyp-overlay (beg end h buf) + (let ((ov (make-overlay beg end buf))) + (when ov + (overlay-put ov 'evaporate t) + (overlay-put ov 'is-hyp t) + (overlay-put ov 'hyp-name h)) + ov)) + +(defun coq-hypcross-unfolded-string() + (propertize + "-" + 'face 'coq-button-face + 'mouse-face 'coq-button-face-pressed)) + +(defun coq-hypcross-folded-string() + (propertize + "+" + 'face 'coq-button-face + 'mouse-face 'coq-button-face-pressed)) + +;; hypcross is displayerd with a "-" when unfolded and a "+" when unfolded. +;; It is highlighted when hovered, is clickable and have a special +;; keymap (f toggles folding, h toggles highlighting...). +;; PC: using button faces of make-button makes the button larger than a +;; characters, which messes columns. So we use simple background colors in +;; coq-hyp...faces +(defun coq-make-hypcross-overlay (beg end h buf) + (let ((ov (make-overlay beg end buf))) + (when ov + (overlay-put ov 'evaporate t) + (overlay-put ov 'is-hypcross t) + (overlay-put ov 'hyp-name h) + (overlay-put ov 'keymap coq-hypcross-map) + (overlay-put ov 'display (coq-hypcross-unfolded-string)) + ;(overlay-put ov 'face 'coq-button-face) + ;(overlay-put ov 'mouse-face 'coq-button-face-pressed) + ;(overlay-put ov 'width .6) + ;(overlay-put ov 'height -1) + (when (eq coq-hypcross-hovering-help t) + (overlay-put ov 'help-echo "mouse-3: unfold; mouse-2 copy name"))) + ov)) + +;; Once we have created the 3 overlays, each recieves a reference to the 2 +;; others. +(defun coq-hyp-overlay-build-cross-refs (hypnameov hypov crosshypov) + (overlay-put hypnameov 'hypcross-ov crosshypov) + (overlay-put hypov 'hypcross-ov crosshypov) + (overlay-put hypnameov 'hyp-ov hypov) + (overlay-put crosshypov 'hyp-ov hypov) + (overlay-put hypov 'hypname-ov hypnameov) + (overlay-put crosshypov 'hypname-ov hypnameov)) + +(defun coq-build-hyp-overlay (hyp-positions buf) + (let* ((names (car hyp-positions)) + (fstname (car names)) + (positions (cdr hyp-positions)) + (begcross (car positions)) + (beghypname (cadr positions)) + (endhypname (caddr positions)) + (beg (cadddr positions)) + (end (cadddr (cdr positions)))) + (let ((hypnameov (coq-make-hypname-overlay beghypname endhypname fstname buf)) + (hypov (coq-make-hyp-overlay beg end fstname buf)) + (crosshypov (coq-make-hypcross-overlay begcross (+ 1 begcross) fstname buf)) + res) + (coq-hyp-overlay-build-cross-refs hypnameov hypov crosshypov) + (mapc + (lambda (s) + (setq res + (cons + (cons (substring-no-properties s) + (cons hypov (cons hypnameov (cons crosshypov nil)) )) + res))) + names) + res))) + +(defun coq-build-hyps-overlays (hyp-positions buf) + (let ((res)) + (mapc (lambda (x) (let ((lassoc (coq-build-hyp-overlay x buf))) + (setq res (append lassoc res)))) + hyp-positions) + res)) + +; builds the list of names from one hyp position (which may contained several +; hyp names) +(defun coq-build-hyp-name (hyp-positions) + (let* ((names (car hyp-positions)) + res) + (mapc (lambda (s) (setq res (cons (substring-no-properties s) res))) names) + res)) + +;; Build the list of hyps names +(defun coq-build-hyps-names (hyp-positions) + (let ((res)) + (mapc (lambda (x) (let ((lassoc (coq-build-hyp-name x))) + (setq res (append lassoc res)))) + hyp-positions) + res)) + + +(defun coq-detect-hyps-in-goals () + "Detect all hypotheses displayed in goals buffer and create overlays. +Three overlays are created for each hyp: (hypov hypnameov hypcrossov), +respectively for the whole hyp, only its name and the overlay for +fold/unfold cross. Return the list of mappings hypname -> overlays." + (let* + ((fsthyp-pos (coq-find-first-hyp)) + (fsthyp-ov (when fsthyp-pos (with-current-buffer proof-goals-buffer + (overlays-at fsthyp-pos)))) + ; is there at least one hyp overlay there? + (fsthyp-hypov (when fsthyp-ov + (cl-some (lambda(x) (overlay-get x 'hyp-name)) + fsthyp-ov)))) + (if fsthyp-hypov coq-hyps-positions ;overlays are already there + (coq-build-hyps-overlays (coq-detect-hyps-positions-in-goals) proof-goals-buffer)))) + +(defun coq-find-hyp-overlay (h) + (cadr (assoc h coq-hyps-positions))) + +;;;;;;;;;;;;;; Highlighting hypothesis ;;;;;;;; +;; Feature: highlighting of hyptohesis that remains when the cript is played +;; (and goals buffer is updated). + +;; On by default. This only works with the SearchAbout function for now. +(defvar coq-highlight-hyps-cited-in-response t + "If non-nil, try to highlight in goals buffers hyps cited in response.") + +;; We maintain a list of hypothesis names that must be highlighted at each +;; regeneration of goals buffer. +(defvar coq-highlighted-hyps nil + "List of hypothesis names that must be highlighted. +These are rehighlighted at each regeneration of goals buffer +using a hook in `proof-shell-handle-delayed-output-hook'.") + +(defun coq-highlight-hyp-aux (h) + "Auxiliary function, use `coq-highlight-hyp' for sticky highlighting. +Unless you want the highlighting to disappear after the goals +buffer is updated." + (let ((hyp-overlay (coq-find-hyp-overlay h))) + (when hyp-overlay + (overlay-put hyp-overlay 'face '(:background "lavender"))))) + +(defun coq-unhighlight-hyp-aux (h) + "Auxiliary function, use `coq-unhighlight-hyp' for sticky highlighting. +Unless you want the highlighting to disappear after the goals +buffer is updated." + (let* ((hyp-overlay (coq-find-hyp-overlay h))) + (when hyp-overlay + (overlay-put hyp-overlay 'face nil)))) + +(defun coq-highlight-hyp (h) + "Highlight hypothesis named H (sticky). +use `coq-unhighlight-hyp' to unhilight." + (unless (member h coq-highlighted-hyps) + (setq coq-highlighted-hyps (cons h coq-highlighted-hyps))) + (coq-highlight-hyp-aux h)) + +(defun coq-unhighlight-hyp (h) + "Unhighlight hypothesis named H." + (when (member h coq-highlighted-hyps) + (setq coq-highlighted-hyps (delete h coq-highlighted-hyps)) + (coq-unhighlight-hyp-aux h))) + +(defun coq-highlight-hyps (lh) + (mapc 'coq-highlight-hyp lh)) + +(defun coq-unhighlight-hyps (lh) + (mapc 'coq-unhighlight-hyp-aux lh)) + +(defun coq-highlight-selected-hyps () + "Highlight all hyps stored in `coq-highlighted-hyps'. +This used in hook to rehilight hypothesis after goals buffer is +updated." + (interactive) + (coq-highlight-hyps coq-highlighted-hyps)) + +(defun coq-unhighlight-selected-hyps () + "Unhighlight all hyps stored in `coq-highlighted-hyps'. +This used before updating `coq-highlighted-hyps' with a new set +of hypothesis to highlight." + (interactive) + (coq-unhighlight-hyps coq-highlighted-hyps) + (setq coq-highlighted-hyps nil)) + +(defun coq-get-hyps-cited-in-response () + "Returns locations of hyps in goals buffer that are cited in response buffer. +See `coq-highlight-hyps-cited-in-response' and `SearchAbout'." + (let* ((hyps-cited-pos (coq-detect-hyps-positions proof-response-buffer)) + (hyps-cited (coq-build-hyps-names hyps-cited-pos))) + (remove-if-not + (lambda (e) + (cl-some;seq-find + (lambda (f) + (string-equal (car e) f)) + hyps-cited)) + coq-hyps-positions))) + +(defun coq-highlight-hyps-cited-in-response () + "Highlight hypothesis cited in response buffer. +Highlight always takes place in goals buffer." + (let ((inters (coq-get-hyps-cited-in-response))) + (coq-unhighlight-selected-hyps) + (setq coq-highlighted-hyps (mapcar 'car inters)) + (coq-highlight-selected-hyps))) + +(defun coq-toggle-highlight-hyp (h) + "Toggle the highlighting status of hypothesis H. +See `coq-highlight-hyp'." + (interactive "sHypothesis name to highlight:") + (if (member h coq-highlighted-hyps) + (coq-unhighlight-hyp h) + (coq-highlight-hyp h))) + +(defun coq-toggle-highlight-hyp-at (pt) + "Toggle hiding the hypothesis at point." + (interactive) + (let* ((ov + (or (car (coq-overlays-at pt 'hyp-name)) + ;; we may be between hypname and hyp, so skip backward to + ;; something meaningful + (save-excursion + (goto-char pt) + (search-backward-regexp "[^ :=]\\|\n") + (car (coq-overlays-at (point) 'hyp-name))))) + (hypname (and ov + (overlay-get ov 'hyp-name)))) + (when hypname + (if (member hypname coq-highlighted-hyps) + (coq-unhighlight-hyp hypname) + (coq-highlight-hyp hypname))))) + +(defun coq-toggle-highlight-hyp-at-point () + (interactive) + (coq-toggle-highlight-hyp-at (point))) -(defvar coq-highlight-id-last-regexp nil) -(defun coq-highlight-id-in-goals (re) - (with-current-buffer proof-goals-buffer - (highlight-regexp re 'lazy-highlight))) +(defun coq-insert-at-point-hyp-at-mouse (event) + (interactive "e") + (let ((hyp-name (save-excursion + (with-current-buffer proof-goals-buffer + (save-excursion + (overlay-get (car (overlays-at (posn-point (event-start event)))) + 'hyp-name)))))) + (insert hyp-name))) -(defun coq-unhighlight-id-in-goals (re) - (with-current-buffer proof-goals-buffer - (unhighlight-regexp re))) +;;;;;;;;;;; Hiding Hypothesis ;;;;;;;;;;; +(defvar coq-hidden-hyp-map (make-sparse-keymap) "Keymap for hidden hypothesis.") -(defun coq-highlight-id-at-pt-in-goals () +(defvar coq-hidden-hyps nil + "List of hypothesis that should be hidden in goals buffer. +These are re-hidden at each regeneration of goals buffer +using a hook in `proof-shell-handle-delayed-output-hook'.") + + +(defun coq-toggle-fold-hyp-at (pt) + "Toggle hiding the hypothesis at point." (interactive) - (let* ((id (coq-id-or-notation-at-point)) - (re (regexp-quote (or id "")))) - (when coq-highlight-id-last-regexp - (coq-unhighlight-id-in-goals coq-highlight-id-last-regexp)) - (coq-highlight-id-in-goals re) - (setq coq-highlight-id-last-regexp re))) + (let* ((ov (car (coq-overlays-at pt 'hyp-name))) + (hypname (and ov (overlay-get ov 'hyp-name)))) + (when hypname + (if (member hypname coq-hidden-hyps) + (coq-unfold-hyp hypname) + (coq-fold-hyp hypname))))) + +(defun coq-toggle-fold-hyp-at-point () + (interactive) + (coq-toggle-fold-hyp-at (point))) +(defun coq-toggle-fold-hyp-at-mouse (event) + "Toggle hiding the hypothesis at mouse click. +Used on hyptohesis overlays in goals buffer mainly." + (interactive "e") + (save-excursion + (with-current-buffer proof-goals-buffer + (save-excursion (coq-toggle-fold-hyp-at (posn-point (event-start event))))))) + +(defun coq-configure-hyp-overlay-hidden (hyp-overlay h) + (when hyp-overlay + (let* ((lgthhyp (- (overlay-end hyp-overlay) (overlay-start hyp-overlay))) + (prefx (make-string (min 8 lgthhyp) ?.)) + (hypcross-ov (overlay-get hyp-overlay 'hypcross-ov))) + (overlay-put + hyp-overlay 'display + prefx ;(propertize prefx 'keymap coq-hidden-hyp-map) + ) + (overlay-put hyp-overlay 'evaporate t) + (overlay-put hyp-overlay 'mouse-face 'proof-command-mouse-highlight-face) + (overlay-put hyp-overlay 'help-echo "mouse-3: unfold; mouse-2 copy name") + (overlay-put hyp-overlay 'hyp-name h) + (overlay-put hyp-overlay 'keymap coq-hidden-hyp-map) + (overlay-put hypcross-ov 'display (coq-hypcross-folded-string))))) + +(defun coq-configure-hyp-overlay-visible (hyp-overlay h) + (when hyp-overlay + (overlay-put hyp-overlay 'display nil) + (overlay-put hyp-overlay 'evaporate t) + (overlay-put hyp-overlay 'mouse-face nil) + (overlay-put hyp-overlay 'help-echo nil) + (overlay-put hyp-overlay 'keymap nil) + (overlay-put (overlay-get hyp-overlay 'hypcross-ov) 'display (coq-hypcross-unfolded-string)))) + +(defun coq-fold-hyp-aux (h) + "Fold hypothesis H's type from the context temporarily. +Displays \".......\" instead. This function relies on variable +coq-hyps-positions. The hiding is cancelled as soon as the goals +buffer is changed, consider using `coq-fold-hyp' if you want the +hiding to be maintain when scripting/undoing." + (let ((hyp-overlay (coq-find-hyp-overlay h))) + (when hyp-overlay (coq-configure-hyp-overlay-hidden hyp-overlay h)))) + +(defun coq-fold-hyp (h) + "Fold hypothesis H's type from the context durably. +\(displays \".......\" instead). This function relies on variable +‘coq-hyps-positions’. The hiding maintained as the goals buffer is +changed, thanks to a hook on `proof-shell-handle-delayed-output-hook', +consider using `coq-fold-hyp' if you want the hiding to be maintain +when scripting/undoing." + (interactive) + (unless (member h coq-hidden-hyps) + (setq coq-hidden-hyps (cons h coq-hidden-hyps)) + (coq-fold-hyp-aux h))) + +(defun coq-unfold-hyp-aux (h) +"Unfold hypothesis H temporarily. +See `coq-fold-hyp-aux'." + (let ((hyp-overlay (coq-find-hyp-overlay h))) + (coq-configure-hyp-overlay-visible hyp-overlay h))) + +(defun coq-unfold-hyp (h) +"Unfold hypothesis H durably. +See `coq-fold-hyp'." + (interactive) + (when (member h coq-hidden-hyps) + (setq coq-hidden-hyps (delete h coq-hidden-hyps)) + (coq-unfold-hyp-aux h))) + +(defun coq-unfold-hyp-list (lh) + "Fold the type of hypothesis in LH temporarily. +See `coq-unfold-hyp-aux'." + (mapc 'coq-unfold-hyp-aux lh)) + +(defun coq-fold-hyp-list (lh) + "Fold the type of hypothesis in LH temporarily. +See `coq-fold-hyp-aux'." + (mapc 'coq-fold-hyp-aux lh)) + +(defun coq-fold-hyps () + "Fold the type of hypothesis in LH durably. +See `coq-fold-hyp'." + (interactive) + (coq-fold-hyp-list coq-hidden-hyps)) + + +(defun coq-unfold-hyps () + "Unfold the type of hypothesis in LH durably. +See `coq-unfold-hyp'." + (interactive) + (coq-unfold-hyp-list coq-hidden-hyps) + (setq coq-hidden-hyps nil)) + +(defun coq-toggle-fold-hyp (h) + "Toggle the hiding status of hypothesis H (asked interactively). +See `coq-fold-hyp'." + (interactive "sHypothesis to fold: ") + (if (member h coq-hidden-hyps) + (coq-unfold-hyp h) + (coq-fold-hyp h))) +;;;;;;; (proof-definvisible coq-PrintHint "Print Hint. ") @@ -1367,6 +1786,10 @@ goal is redisplayed." (proof-definvisible coq-unset-printing-synth "Unset Printing Synth.") (proof-definvisible coq-set-printing-coercions "Set Printing Coercions.") (proof-definvisible coq-unset-printing-coercions "Unset Printing Coercions.") +(proof-definvisible coq-set-printing-compact-contexts "Set Printing Compact Contexts.") +(proof-definvisible coq-unset-printing-compact-contexts "Unset Printing Compact Contexts.") +(proof-definvisible coq-set-printing-unfocused "Set Printing Unfocused.") +(proof-definvisible coq-unset-printing-unfocused "Unset Printing Unfocused.") (proof-definvisible coq-set-printing-universes "Set Printing Universes.") (proof-definvisible coq-unset-printing-universes "Unset Printing Universes.") (proof-definvisible coq-set-printing-wildcards "Set Printing Wildcard.") @@ -1433,15 +1856,17 @@ goal is redisplayed." (defun coq-get-comment-region (pt) - "Return a list of the forme (beg end) where beg,end is the comment region arount position PT. -Return nil if PT is not inside a comment" + "Return a list of the form (BEG END). +BEG,END being the comment region arount position PT. +Return nil if PT is not inside a comment." (save-excursion (goto-char pt) `(,(save-excursion (coq-find-comment-start)) ,(save-excursion (coq-find-comment-end))))) (defun coq-near-comment-region () - "Return a list of the forme (beg end) where beg,end is the comment region near position PT. + "Return a list of the forme (BEG END). +BEG,END being is the comment region near position PT. Return nil if PT is not near a comment. Near here means PT is either inside or just aside of a comment." (save-excursion @@ -1671,7 +2096,7 @@ Near here means PT is either inside or just aside of a comment." ;; want xml like tags, and I want them removed before warning display. ;; I want the same for errors -> pgip - proof-shell-eager-annotation-end "\377\\|done\\]\\|</infomsg>\\|\\*\\*\\*\\*\\*\\*\\|) >" ; done + proof-shell-eager-annotation-end coq-shell-eager-annotation-end ; done proof-shell-annotated-prompt-regexp coq-shell-prompt-pattern proof-shell-result-start "\372 Pbp result \373" proof-shell-result-end "\372 End Pbp result \373" @@ -1808,7 +2233,7 @@ Near here means PT is either inside or just aside of a comment." (defpacustom search-blacklist coq-search-blacklist-string - "Strings to blacklist in requests to coq environment." + "Strings to blacklist in requests to Coq environment." :type 'string :get 'coq-get-search-blacklist :setting coq-set-search-blacklist) @@ -1838,7 +2263,7 @@ Near here means PT is either inside or just aside of a comment." (defun coq-extract-instantiated-existentials (start end) "Coq specific function for `proof-tree-extract-instantiated-existentials'. -Returns the list of currently instantiated existential variables." +Return the list of currently instantiated existential variables." (proof-tree-extract-list start end coq-proof-tree-existentials-state-start-regexp @@ -1851,11 +2276,11 @@ Returns the list of currently instantiated existential variables." (defun coq-proof-tree-get-new-subgoals () "Check for new subgoals and issue appropriate Show commands. -This is a hook function for `proof-tree-urgent-action-hook'. This +This is a hook function for `proof-tree-urgent-action-hook'. This function examines the current goal output and searches for new -unknown subgoals. Those subgoals have been generated by the last +unknown subgoals. Those subgoals have been generated by the last proof command and we must send their complete sequent text -eventually to prooftree. Because subgoals may change with +eventually to prooftree. Because subgoals may change with the next proof command, we must execute the additionally needed Show commands before the next real proof command. @@ -1863,18 +2288,18 @@ The ID's of the open goals are checked with `proof-tree-sequent-hash' in order to find out if they are new. For any new goal an appropriate Show Goal command with a 'proof-tree-show-subgoal flag is inserted into -`proof-action-list'. Then, in the normal delayed output +`proof-action-list'. Then, in the normal delayed output processing, the sequent text is send to prooftree as a sequent update (see `proof-tree-update-sequent') and the ID of the sequent is registered as known in `proof-tree-sequent-hash'. Searching for new subgoals must only be done when the proof is not finished, because Coq 8.5 lists open existential variables -as (new) open subgoals. For this test we assume that +as (new) open subgoals. For this test we assume that `proof-marker' has not yet been moved. The `proof-tree-urgent-action-hook' is also called for undo -commands. For those, nothing is done. +commands. For those, nothing is done. The not yet delayed output is in the region \[proof-shell-delayed-output-start, proof-shell-delayed-output-end]." @@ -1958,9 +2383,9 @@ This is the Coq incarnation of `proof-tree-find-undo-position'." (defun coq-proof-tree-enable-evar-callback (span) "Callback for the evar printing status test. -This is the callback for the command ``Test Printing Dependent -Evars Line''. It checks whether evar printing was off and -remembers that fact in `coq--proof-tree-must-disable-evars'." +This is the callback for the command ``Test Printing Dependent Evars Line''. +It checks whether evar printing was off and remembers that +fact in `coq--proof-tree-must-disable-evars'." (with-current-buffer proof-shell-buffer (save-excursion ;; When the callback runs, the next item is sent to Coq already and @@ -2001,11 +2426,11 @@ properly after the proof and enable the evar printing." (defun coq-proof-tree-disable-evars () "Disable evar printing if necessary. This function switches off evar printing after the proof, if it -was off before the proof. For undo commands, we rely on the fact +was off before the proof. For undo commands, we rely on the fact that Coq itself undos the effect of the evar printing change that -we inserted after the goal statement. We also rely on the fact +we inserted after the goal statement. We also rely on the fact that Proof General never backtracks into the middle of a -proof. (If this would happen, Coq would switch evar printing on +proof. (If this would happen, Coq would switch evar printing on and the code here would not switch it off after the proof.) Being called from `proof-tree-urgent-action-hook', this function @@ -2019,10 +2444,10 @@ result of `coq-proof-tree-get-proof-info'." (defun coq-proof-tree-evar-display-toggle () "Urgent action hook function for changing the evar printing status in Coq. This function is for `proof-tree-urgent-action-hook' (which is -called only if external proof disaply is switched on). It checks +called only if external proof disaply is switched on). It checks whether a proof was started or stopped and inserts commands for enableing and disabling the evar status line for Coq 8.6 or -later. Without the evar status line being enabled, prooftree +later. Without the evar status line being enabled, prooftree crashes. Must only be called via `proof-tree-urgent-action-hook' to ensure @@ -2194,7 +2619,8 @@ mouse activation." (defun coq--format-intros (output) "Create an “intros” form from the OUTPUT of “Show Intros”." - (let* ((shints (replace-regexp-in-string "[\r\n ]*\\'" "" output))) + (let* ((shints1 (replace-regexp-in-string "^[0-9] subgoal\\(.\\|\n\\|\r\\)*" "" output)) + (shints (replace-regexp-in-string "[\r\n ]*\\'" "" shints1))) (if (or (string= "" shints) (string-match coq-error-regexp shints)) (error "Don't know what to intro") @@ -2225,7 +2651,7 @@ tacitcs like destruct and induction reuse hypothesis names by default, which makes the detection of new hypothesis incorrect. the hack consists in adding the \"!\" modifier on the argument destructed, so that it is left in the goal and the name cannot be -reused. We also had a \"clear\" at the end of the tactic so that +reused. We also had a \"clear\" at the end of the tactic so that the whole tactic behaves correctly. Warning: this makes the error messages (and location) wrong.") @@ -2361,6 +2787,21 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (proof-shell-invisible-command q)))) +;; TODO SearchAbout become Search in v8.5, change when V8.4 becomes old. +(defun coq-SearchAbout () + (interactive) + (coq-ask-do + ;; TODO: use [Add Search Blacklist "foo"] to exclude optionaly some patterns: + ;; "_ind" "_rec" "R_" "_equation" + "SearchAbout (ex: \"eq_\" eq -bool)" + "SearchAbout" + nil nil t) + (when coq-highlight-hyps-cited-in-response + (coq-highlight-hyps-cited-in-response) + (message "M-x coq-unhighlight-selected-hyps to remove highlighting, [Coq/Settings/Search Blacklist] to change blacklisting.")) + (unless coq-highlight-hyps-cited-in-response + (message "[Coq/Settings/Search Blacklist] to change blacklisting."))) + ;; Insertion commands (define-key coq-keymap [(control ?i)] 'coq-insert-intros) (define-key coq-keymap [(control ?m)] 'coq-insert-match) @@ -2410,6 +2851,11 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?w)] 'coq-ask-adapt-printing-width-and-show) (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?l)] 'coq-LocateConstant) (define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?n)] 'coq-LocateNotation) +;; specific to goals buffer: (un)foldinng and (un)highlighting shortcuts +(define-key coq-goals-mode-map [?f] 'coq-toggle-fold-hyp-at-point) +(define-key coq-goals-mode-map [?F] 'coq-unfold-hyps) +(define-key coq-goals-mode-map [?h] 'coq-toggle-highlight-hyp-at-point) +(define-key coq-goals-mode-map [?H] 'coq-unhighlight-selected-hyps) (define-key coq-response-mode-map [(control ?c)(control ?a)(control ?c)] 'coq-Check) @@ -2448,6 +2894,27 @@ Completion is on a quasi-exhaustive list of Coq tacticals." (define-key proof-goals-mode-map [(control shift down-mouse-1)] 'coq-id-under-mouse-query) (define-key proof-goals-mode-map [(control shift mouse-1)] '(lambda () (interactive)))) + + +;; Default binding on hypothesis names: clicking on the name of an hyp with +;; button 3 folds it. Click on it with button 2 copies the names at current +;; point. +(when coq-hypname-map + (define-key coq-hypname-map [(mouse-3)] 'coq-toggle-fold-hyp-at-mouse) + (define-key coq-hypname-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse)) + +;; Default binding: clicking on the cross to folds/unfold hyp. +;; Click on it with button 2 copies the names at current point. +(when coq-hypname-map + (define-key coq-hypcross-map [(mouse-1)] 'coq-toggle-fold-hyp-at-mouse) + (define-key coq-hypcross-map [return] 'coq-toggle-fold-hyp-at-point) + (define-key coq-hypcross-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse)) +;; Ddefault binding: clicking on a hidden hyp with button 3 unfolds it, with +;; button 2 it copies hyp name at current point. +(when coq-hidden-hyp-map + (define-key coq-hidden-hyp-map [(mouse-3)] 'coq-toggle-fold-hyp-at-mouse) + (define-key coq-hidden-hyp-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse)) + ;;;;;;;;;;;;;;;;;;;;;;;; ;; error handling ;;;;;;;;;;;;;;;;;;;;;;;; @@ -2513,8 +2980,9 @@ buffer." (defun coq-highlight-error (&optional parseresp clean) - "Parses the last coq output looking at an error message. Highlight the text -pointed by it. Coq error message must be like this: + "Parse the last Coq output looking at an error message. +Highlight the text pointed by it. +Coq error message must be like this: \" > command with an error here ... @@ -2593,7 +3061,7 @@ number of hypothesis displayed, without hiding the goal" (with-selected-window goal-win ;; find snd goal or buffer end, if not found this goes to the ;; end of buffer - (search-forward-regexp "subgoal 2\\|\\'") + (search-forward-regexp "subgoal 2\\|\\*\\*\\* Unfocused goals:\\|\\'") (beginning-of-line) ;; find something backward else than a space: bottom of concl (ignore-errors (search-backward-regexp "\\S-")) @@ -2650,6 +3118,14 @@ number of hypothesis displayed, without hiding the goal" proof-shell-last-output) (proof-clean-buffer proof-goals-buffer)))) +(add-hook 'proof-shell-handle-delayed-output-hook + (lambda () + (setq coq-hyps-positions (coq-detect-hyps-in-goals)) + (coq-highlight-selected-hyps) + (coq-fold-hyps) + )) + + (defun is-not-split-vertic (selected-window) (<= (- (frame-height) (window-height)) 2)) @@ -2720,24 +3196,24 @@ Only when three-buffer-mode is enabled." (defcustom coq-double-hit-enable nil "* Experimental: Whether or not double hit should be enabled in coq mode. -A double hit is performed by pressing twice a key quickly. If +A double hit is performed by pressing twice a key quickly. If this variable is not nil, then 1) it means that electric terminator is off and 2) a double hit on the terminator act as -the usual electric terminator. See `proof-electric-terminator'. -" +the usual electric terminator. See `proof-electric-terminator'." :type 'boolean :set 'proof-set-value :group 'proof-user-options) (defvar coq-double-hit-hot-key "." - "The key used for double hit electric terminator. By default this -is the coq terminator \".\" key. For example one can do this: + "The key used for double hit electric terminator. +By default this is the coq terminator \".\" key. +For example one can do this: -(setq coq-double-hit-hot-key (kbd \";\")) +\(setq coq-double-hit-hot-key (kbd \";\")) -to use semi-colon instead (on french keyboard, it is the same key -as \".\" but without shift.") +to use semi-colon instead (on French keyboard, it is the same key as +\".\" but without shift.") (defvar coq-double-hit-hot-keybinding nil "The keybinding that was erased by double hit terminator enabling. @@ -2778,7 +3254,7 @@ This is an advice to pg `proof-electric-terminator-enable' function." "The maximum delay between the two hit of a double hit in coq/proofgeneral.") (defvar coq-double-hit-timer nil - "the timer used to watch for double hits.") + "The timer used to watch for double hits.") (defvar coq-double-hit-hot nil "The variable telling that a double hit is still possible.") @@ -2786,8 +3262,8 @@ This is an advice to pg `proof-electric-terminator-enable' function." (defun coq-unset-double-hit-hot () - "Disable timer `coq-double-hit-timer' and set it to nil. Shut -off the current double hit if any. This function is supposed to + "Disable timer `coq-double-hit-timer' and set it to nil. +Shut off the current double hit if any. This function is supposed to be called at double hit timeout." (when coq-double-hit-timer (cancel-timer coq-double-hit-timer)) (setq coq-double-hit-hot nil) @@ -2810,9 +3286,11 @@ Starts a timer for a double hit otherwise." nil 'coq-unset-double-hit-hot)))) (defun coq-terminator-insert (&optional count) - "A wrapper on `proof-electric-terminator' to accept double hits instead if enabled. -If by accident `proof-electric-terminator-enable' and `coq-double-hit-enable' -are non-nil at the same time, this gives priority to the former." + "A wrapper on `proof-electric-terminator'. +Used to accept double hits instead if enabled. +If by accident option `proof-electric-terminator-enable' and option +`coq-double-hit-enable' are non-nil at the same time, this gives +priority to the former." (interactive) (if (and (not proof-electric-terminator-enable) coq-double-hit-enable (null count)) @@ -2829,13 +3307,6 @@ are non-nil at the same time, this gives priority to the former." (define-key coq-mode-map (kbd ".") 'coq-terminator-insert) ;(define-key coq-mode-map (kbd ";") 'coq-terminator-insert) ; for french keyboards -;; Activation of ML4PG functionality -(declare-function ml4pg-select-mode "ml4pg") ;; Avoids copilation warnings - -(defun coq-activate-ml4pg () - (let ((filename (concatenate 'string proof-home-directory "contrib/ML4PG/ml4pg.el"))) - (when (file-exists-p filename) (load-file filename) (ml4pg-select-mode)))) - ;;;;;;;;;;;;;; ;; This was done in coq-compile-common, but it is actually a good idea even |