aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
diff options
context:
space:
mode:
Diffstat (limited to 'coq/coq.el')
-rw-r--r--coq/coq.el518
1 files changed, 480 insertions, 38 deletions
diff --git a/coq/coq.el b/coq/coq.el
index aff05d28..96a9bf41 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1,12 +1,23 @@
-;; 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)
@@ -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,12 +101,12 @@ 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
+ "Prefer start of the conclusion over its end when displaying goals
that do not fit in the goals window."
:type 'boolean
:group 'coq)
@@ -432,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
@@ -884,7 +895,7 @@ 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
@@ -935,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)
@@ -1043,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."))
@@ -1063,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)
@@ -1359,26 +1367,411 @@ 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 hypothesis 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.
+Returnns 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-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)))
+
+;;;;;;;;;;; Hiding Hypothesis ;;;;;;;;;;;
+(defvar coq-hidden-hyp-map (make-sparse-keymap) "Keymap for hidden hypothesis")
-(defun coq-highlight-id-in-goals (re)
- (with-current-buffer proof-goals-buffer
- (highlight-regexp re 'lazy-highlight)))
+(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-unhighlight-id-in-goals (re)
- (with-current-buffer proof-goals-buffer
- (unhighlight-regexp re)))
-(defun coq-highlight-id-at-pt-in-goals ()
+(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. ")
@@ -1840,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)
@@ -2394,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)
@@ -2443,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)
@@ -2481,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
;;;;;;;;;;;;;;;;;;;;;;;;
@@ -2626,7 +3060,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-"))
@@ -2683,6 +3117,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))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 20:20:39 +0000