diff --git a/CHANGES b/CHANGES index 1f5edd937..63500e7be 100644 --- a/CHANGES +++ b/CHANGES @@ -60,7 +60,19 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG `coq-run-completely-silent' to switch back to old behavior. Note that external proof tree display is only supported if Coq/Rocq runs completely silent. - +*** `Holes` library removed. + This was a poor man's code template insertion. This is now removed + and see next point below for a replacement. +*** yasnippets default code templates + - if you use company-coq, this is disabled by default because + company-coq uses its own yasnippet templates. + - Templates are defined from coq-syntax.el definitions. No + exhaustivity garanteed. + - You might want to define your own templates instead. + - To opt out from default templates: + (setq coq-yasnippet-use-default-templates nil) + - To out out from yasnippet with proofgeneral: + (setq coq-use-yasnippet nil) * Changes of Proof General 4.5 from Proof General 4.4 diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 3eefa6054..aa23d4774 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -22,9 +22,21 @@ (require 'proof) (require 'coq-syntax) -(defun holes-show-doc () - (interactive) - (describe-function 'holes-mode)) +(defcustom coq-use-yasnippet (and (not (member 'company-coq-mode coq-mode-hook)) + (fboundp 'yas-expand)) + "Should Coq use yasnippets templates. + +Default value is t unless yasnippet is not installed or company-coq +appears in the hoocoq-mode-hook." + :type 'boolean + :group 'coq) + +(defcustom coq-yasnippet-use-default-templates t + "Should Proofgeneral coq mode use its yasnippets default templates. + +Set this to nil if you don't want the default yasnippets templates." + :type 'boolean + :group 'coq) (defun coq-local-vars-list-show-doc () (interactive) @@ -64,10 +76,51 @@ (defconst coq-terms-abbrev-table (coq-build-abbrev-table-from-db coq-terms-db)) +(defun coq-define-yasnippets-from-db () + "Register yas snippets from default proofgeneral coq db. + +yassnippet is a framework for inserting code templates for emacs. This +will add hundreds of yas snippets, generated from proofgeneral list of +coq commands (which is not necessarily always up to date). You probably +want to use your own set of snippets at some point but it is a good +start." + (when (fboundp 'yas-define-snippets) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-tactics-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-solve-tactics-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-solve-cheat-tactics-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-tacticals-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-decl-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-defn-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-goal-starters-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-queries-commands-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-other-commands-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-ssreflect-commands-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-terms-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-user-tactics-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-user-commands-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-user-tacticals-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-user-solve-tactics-db)) + (yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-user-cheat-tactics-db)))) + + +;; this is the function called by insertion menus. TODO: separate +;; these menus from yasnippet templates because this should work even +;; if the user has its own templates instead of the default ones. +(defun coq-insert-template (snippet) + "Expand template ABBR using (by priority) yasnippet, abbrev or just ALT." + (when snippet + (if (and coq-use-yasnippet (fboundp 'yas-expand)) + (yas-expand-snippet (coq-yas-snippet-from-db snippet)) + (insert (coq-simple-abbrev-from-db snippet))))) + + ;; (if (fboundp 'with-undo-amalgamate) ;; emacs > 29.1 + ;; (with-undo-amalgamate (insert abbr) (yas-expand)) + ;; (progn (insert abbr) (yas-expand))) + + ;;; The abbrev table built from keywords tables -;#s and @{..} are replaced by holes by holes-abbrev-complete (define-abbrev-table 'coq-mode-abbrev-table (append coq-tactics-abbrev-table coq-tacticals-abbrev-table coq-commands-abbrev-table coq-terms-abbrev-table) diff --git a/coq/coq-db.el b/coq/coq-db.el index 680292d16..6f1b04121 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -25,7 +25,6 @@ (eval-when-compile (require 'cl-lib)) ;decf -(require 'holes) (require 'diff-mode) (defconst coq-syntax-db nil @@ -88,7 +87,8 @@ the first hole even if more than one." (pt (point))) (if f (funcall f) ; call f if present (insert (or s tac)) ; insert completion and indent otherwise - (holes-replace-string-by-holes-backward-jump pt nil alwaysjump) + ;; FIXHOLE + ;;(holes-replace-string-by-holes-backward-jump pt nil alwaysjump) (indent-according-to-mode)))) @@ -184,7 +184,8 @@ of the largest line in the menu (without abbrev and shortcut specifications). Used by `coq-build-menu-from-db', which you should probably use instead. See `coq-syntax-db' for DB structure." (let ((l db) (res ()) (size lgth) - (keybind-abbrev (substitute-command-keys " \\[expand-abbrev]"))) + (keybind-abbrev (if coq-use-yasnippet (substitute-command-keys " \\[yas-expand]") + (substitute-command-keys " \\[expand-abbrev]")))) (while (and l (> size 0)) (let* ((hd (pop l)) (menu (nth 0 hd)) ; e1 = menu entry @@ -192,7 +193,7 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See (complt (nth 2 hd)) ; e3 = completion ;; (state (nth 3 hd)) ; e4 = state changing ;; (color (nth 4 hd)) ; e5 = colorization string - (insertfn (nth 5 hd)) ; e6 = function for smart insertion + ;; (insertfn (nth 5 hd)) ; e6 = function for smart insertion not used (menuhide (nth 6 hd)) ; e7 = if non-nil : hide in menu (entry-with (max (- menuwidth (length menu)) 0)) (spaces (make-string entry-with ? )) @@ -205,8 +206,7 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See (concat menu (if (not abbrev) "" (concat spaces "(" abbrev keybind-abbrev ")"))) - ;;insertion function if present otherwise insert completion - (if insertfn insertfn `(holes-insert-and-expand ,complt)) + `(coq-insert-template ,complt) t))) (push menu-entry res))) (cl-decf size))) @@ -250,10 +250,9 @@ structure." (setq lgth (length l))) res)) -(defcustom coq-holes-minor-mode t - "*Whether to apply holes minor mode (see `holes-show-doc') in coq mode." - :type 'boolean - :group 'coq) +(defun coq-simple-abbrev-from-db (s) + "Returns the coq db abbrevitaion string S cleaned from template markups." + (if s (replace-regexp-in-string "#\\|@{\\(?1:[^{}]*\\)}" "" s))) (defun coq-build-abbrev-table-from-db (db) "Take a keyword database DB and return an abbrev table. @@ -264,12 +263,47 @@ See `coq-syntax-db' for DB structure." (_e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation (e3 (car tl2)) (_tl3 (cdr tl2)) ; e3 = completion - ) + (e3clean (coq-simple-abbrev-from-db e3))) + ;; careful: nconc destructive! + (when e2 (push `(,e2 ,e3clean nil :system t) res)) + (setq l tl))) + (nreverse res))) + + +(defun coq-db--replace-abbrev-yas (i mtch) + "Translationi of a coq db abbrev spec to a yasnippet one." + (cond + ;; FIXME: define a "end point for the snippet: that is the place where the + ;; cursor should go after fiolling the holes. Generally it is the place where + ;; you want to continue editing. + ((string-equal mtch "#") (concat "$" (int-to-string i))) + (t (concat "${" (int-to-string i) ":" (match-string 1 mtch) "}")) + ) + ) + +(defun coq-yas-snippet-from-db (s) + "Translate the coq db abbrevitaion string S into the yasnippet abbrev format." + (if s + (let ((cpt 0)) + (replace-regexp-in-string + "#\\|@{\\(?1:[^{}]*\\)}" + (lambda (mtch) (setq cpt (+ 1 cpt)) (coq-db--replace-abbrev-yas cpt mtch)) + s)))) + +(defun coq-yas-snippet-table-from-db (db) + "Take a keyword database DB and return a list of yasnippets. + +The list contains lists or args to be given to yas-define-snippets. +See `coq-syntax-db' for DB structure." + (let ((l db) (res ())) + (while l + (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 + (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry + (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation + (e3 (car tl2)) (_tl3 (cdr tl2)) ; e3 = completion + (yas_e3 (coq-yas-snippet-from-db e3))) ;; careful: nconc destructive! - (when e2 - (push `(,e2 ,e3 ,(if coq-holes-minor-mode #'holes-abbrev-complete) - :system t) - res)) + (when e2 (push `(,e2 ,yas_e3 ,e1) res)) (setq l tl))) (nreverse res))) diff --git a/coq/coq-mode.el b/coq/coq-mode.el index 3842bbefc..4c9d8d581 100644 --- a/coq/coq-mode.el +++ b/coq/coq-mode.el @@ -235,10 +235,6 @@ Near here means PT is either inside or just aside of a comment." ;; we can cope with nested comments (set (make-local-variable 'comment-quote-nested) nil) - ;; FIXME: have abbreviation without holes - ;(if coq-use-editing-holes (holes-mode 1)) - (if (fboundp 'holes-mode) (holes-mode 1)) - ;; Setup Proof-General interface to Coq. (if coq-use-pg (coq-pg-setup)) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index c66b8107a..7ba7fd3a9 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -251,11 +251,10 @@ so for the following reasons: ("now_show" nil "now_show" t "now_show") ("nra" nil "nra" t "nra") ("nsatz" nil "nsatz" t "nsatz") - ("omega" "o" "omega" t "omega") ("pattern" "pat" "pattern" t "pattern") ("pattern(s)" "pats" "pattern # , #" t) ("pattern at" "pata" "pattern # at #" t) - ("pose" "po" "pose ( # := # )" t "pose") + ("pose" "pose" "pose ( # := # )" t "pose") ("prolog" "prol" "prolog" t "prolog") ("psatz" nil "psatz" t "psatz") ("quote" "quote" "quote" t "quote") @@ -268,8 +267,8 @@ so for the following reasons: ("rename into" "ren" "rename # into #" t "rename") ("replace with" "rep" "replace # with #" t "replace") ("replace with in" "repi" "replace # with # in #" t) - ("revert dependent" "r" "revert dependent" t "revert\\s-+dependent") - ("revert" "r" "revert" t "revert") + ("revert dependent" "rd" "revert dependent" t "revert\\s-+dependent") + ("revert" "rev" "revert" t "revert") ("rewrite_all" nil "rewrite_all" t "rewrite_all") ("rewrite_all <-" nil "rewrite_all" t "rewrite_all") ("rewrite <- in" "ri<" "rewrite <- # in #" t) @@ -320,9 +319,9 @@ so for the following reasons: ("nat_norm" "nnorm" "nat_norm" t "nat_norm") ("bool_congr" "bcongr" "bool_congr" t "bool_congr") ("prop_congr" "prcongr" "prop_congr" t "prop_congr") - ("move" "m" "move" t "move") - ("pose" "po" "pose # := #" t "pose") - ("set" "set" "set # := #" t "set") + ("move" "mo" "move" t "move") + ("pose (ssr)" "po" "pose # := #" t "pose(ssr)") + ("set (ssr)" "se" "set # := #" t "set (ssr)") ("have" "hv" "have # : #" t "have") ("congr" "con" "congr #" t "congr") ("wlog" "wlog" "wlog : / #" t "wlog") @@ -499,14 +498,13 @@ so for the following reasons: ("Program Instance" "pinstance" "Program Instance [ # ] => # where \n# := #;\n# := #." t "Program\\s-+Instance") ("Let" "Let" "Let # : # := #." t "Let") ("Local Ltac2" nil "Local Ltac2 # := #." t "Local\\s-+Ltac2") - ("Ltac2 Type" "lt2rty" "Ltac2 Type rec # := #." t "Ltac2 Type rec") + ("Ltac2 Type rec" "lt2rty" "Ltac2 Type rec # := #." t "Ltac2 Type rec") ("Ltac2 Type" "lt2ty" "Ltac2 Type # := #." t "Ltac2 Type") - ("Ltac2 Type" "lt2oty" "Ltac2 Type # ::= #." t "Ltac2 Type") - ("Ltac2 Type" "lt2wty" "Ltac2 Type #." t "Ltac2 Type") - ("Ltac2" "lt2mr" "Ltac2 mutable rec # := #." t "Ltac2 mutable rec") - ("Ltac2" "lt2m" "Ltac2 mutable # := #." t "Ltac2 mutable") - ("Ltac2" "lt2r" "Ltac2 rec # := #." t "Ltac2 rec") - ("Ltac2" "lt2s" "Ltac2 Set # := #." t "Ltac2 Set") + ("Ltac2 Type ::=" "lt2oty" "Ltac2 Type # ::= #." t "Ltac2 Type ::=") + ("Ltac2 mutable rec" "lt2mr" "Ltac2 mutable rec # := #." t "Ltac2 mutable rec") + ("Ltac2 mutable" "lt2m" "Ltac2 mutable # := #." t "Ltac2 mutable") + ("Ltac2 rec" "lt2r" "Ltac2 rec # := #." t "Ltac2 rec") + ("Ltac2 Set" "lt2s" "Ltac2 Set # := #." t "Ltac2 Set") ("Ltac2" "lt2" "Ltac2 # := #." t "Ltac2") ("Local Ltac" nil "Local Ltac # := #." t "Local\\s-+Ltac") ("Ltac" "ltac" "Ltac # := #." t "Ltac") @@ -739,18 +737,19 @@ They deserve a separate menu for sending them to Coq without insertion.") ("Set Maximal Implicit Insertion" nil "Set Maximal Implicit Insertion" t "Set Maximal\\s-+Implicit\\s-+Insertion") ("Set Nonrecursive Elimination Schemes" nil "Set Nonrecursive Elimination Schemes" t "Set Nonrecursive\\s-+Elimination\\s-+Schemes") ("Set Parsing Explicit" nil "Set Parsing Explicit" t "Set Parsing\\s-+Explicit") + ("Set Nested Proofs Allowed" "snpa" "Set Nested Proofs Allowed" t "Set\\s-+Nested\\s-+Proofs\\s-+Allowed") ("Set Primitive Projections" nil "Set Primitive Projections" t "Set Primitive\\s-+Projections") - ("Set Printing All" nil "Set Printing All" t "Set\\s-+Printing\\s-+All") - ("Set Printing Coercions" nil "Set Printing Coercions" t "Set\\s-+Printing\\s-+Coercions") + ("Set Printing All" "spa" "Set Printing All" t "Set\\s-+Printing\\s-+All") + ("Set Printing Coercions" "spc" "Set Printing Coercions" t "Set\\s-+Printing\\s-+Coercions") ("Set Printing Compact Contexts" nil "set Printing Compact Contexts" t "set\\s-+Printing\\s-+Compact\\s-+Contexts") ("Set Printing Depth" nil "Set Printing Depth" t "Set\\s-+Printing\\s-+Depth") ("Set Printing Existential Instances" nil "Set Printing Existential Instances" t "Set\\s-+Printing\\s-+Existential\\s-+Instances") ("Set Printing Goal Tags" nil "Set Printing Goal Tags" t "Set\\s-+Printing\\s-+Goal\\s-+Tags") ("Set Printing Goal Names" nil "Set Printing Goal Names" t "Set\\s-+Printing\\s-+Goal\\s-+Names") - ("Set Printing Implicit" nil "Set Printing Implicit" t "Set\\s-+Printing\\s-+Implicit") + ("Set Printing Implicit" "spi" "Set Printing Implicit" t "Set\\s-+Printing\\s-+Implicit") ("Set Printing Implicit Defensive" nil "Set Printing Implicit Defensive" t "Set\\s-+Printing\\s-+Implicit\\s-+Defensive") ("Set Printing Matching" nil "Set Printing Matching" t "Set\\s-+Printing\\s-+Matching") - ("Set Printing Notations" nil "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") + ("Set Printing Notations" "spn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") ("Set Printing Primitive Projection Compatibility" nil "Set Printing Primitive Projection Compatibility" t "Set\\s-+Printing\\s-+Primitive\\s-+Projection\\s-+Compatibility") ("Set Printing Primitive Projection Parameters" nil "Set Printing Primitive Projection Parameters" t "Set\\s-+Printing\\s-+Primitive\\s-+Projection\\s-+Parameters") ("Set Printing Projections" nil "Set Printing Projections" t "Set\\s-+Printing\\s-+Projections") @@ -867,17 +866,18 @@ They deserve a separate menu for sending them to Coq without insertion.") ("Unset Loose Hint Behavior" nil "Unset Loose Hint Behavior" t "Unset Loose\\s-+Hint\\s-+Behavior") ("Unset Maximal Implicit Insertion" nil "Unset Maximal Implicit Insertion" t "Unset Maximal\\s-+Implicit\\s-+Insertion") ("Unset Nonrecursive Elimination Schemes" nil "Unset Nonrecursive Elimination Schemes" t "Unset Nonrecursive\\s-+Elimination\\s-+Schemes") + ("Unset Nested Proofs Allowed" "usnpa" "Unset Nested Proofs Allowed" t "Unset\\s-+Nested\\s-+Proofs\\s-+Allowed") ("Unset Parsing Explicit" nil "Unset Parsing Explicit" t "Unset Parsing\\s-+Explicit") ("Unset Primitive Projections" nil "Unset Primitive Projections" t "Unset Primitive\\s-+Projections") - ("Unset Printing All" nil "Unset Printing All" t "Unset Printing\\s-+All") + ("Unset Printing All" "uspa" "Unset Printing All" t "Unset Printing\\s-+All") ("Unset Printing Coercions" nil "Unset Printing Coercions" t "Unset\\s-+Printing\\s-+Coercions") ("Unset Printing Compact Contexts" nil "Unset Printing Compact Contexts" t "Unset\\s-+Printing\\s-+Compact\\s-+Contexts") ("Unset Printing Depth" nil "Unset Printing Depth" t "Unset Printing\\s-+Depth") ("Unset Printing Existential Instances" nil "Unset Printing Existential Instances" t "Unset Printing\\s-+Existential\\s-+Instances") - ("Unset Printing Implicit" nil "Unset Printing Implicit" t "Unset Printing\\s-+Implicit") + ("Unset Printing Implicit" "uspi" "Unset Printing Implicit" t "Unset Printing\\s-+Implicit") ("Unset Printing Implicit Defensive" nil "Unset Printing Implicit Defensive" t "Unset Printing\\s-+Implicit\\s-+Defensive") ("Unset Printing Matching" nil "Unset Printing Matching" t "Unset Printing\\s-+Matching") - ("Unset Printing Notations" nil "Unset Printing Notations" t "Unset Printing\\s-+Notations") + ("Unset Printing Notations" "uspn" "Unset Printing Notations" t "Unset Printing\\s-+Notations") ("Unset Printing Primitive Projection Compatibility" nil "Unset Printing Primitive Projection Compatibility" t "Unset Printing\\s-+Primitive\\s-+Projection\\s-+Compatibility") ("Unset Printing Primitive Projection Parameters" nil "Unset Printing Primitive Projection Parameters" t "Unset Printing\\s-+Primitive\\s-+Projection\\s-+Parameters") ("Unset Printing Projections" nil "Unset Printing Projections" t "Unset Printing\\s-+Projections") diff --git a/coq/coq.el b/coq/coq.el index bea74c6a5..0fc0222fb 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -46,7 +46,6 @@ (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) @@ -98,7 +97,7 @@ supported if this option is t." (defcustom coq-user-init-cmd nil "User defined init commands for Coq. These are appended at the end of `coq-shell-init-cmd'." - :type '(repeat (cons (string :tag "command"))) + :type '(repeat string) :group 'coq) (defcustom coq-optimise-resp-windows-enable t @@ -2059,6 +2058,16 @@ at `proof-assistant-settings-cmds' evaluation time.") (setq proof-cannot-reopen-processed-files nil) + (cond + ((and coq-use-yasnippet (not (fboundp 'yas-define-snippets))) + (message "Warning: `coq-use-yasnippet` is t but yasnippet not installed.")) + ((and coq-use-yasnippet (not coq-yasnippet-use-default-templates)) + (message "Default coq yasnippets NOT loaded as asked.")) + (coq-use-yasnippet + (message "Loading default coq yasnippets.") + (coq-define-yasnippets-from-db)) + (t (message "yasnippet not found by proofgeneral, falling back to simple abbrevs"))) + (proof-config-done) ) @@ -2552,17 +2561,17 @@ mouse activation." (typkind (if (string-equal mods "Section") "" ;; if not a section (completing-read "Kind of type (optional, TAB to see list): " - modtype-kinds-table))) - (p (point))) + modtype-kinds-table)))) (if (string-equal typkind "") (progn - (insert mods " " s ".\n#\nEnd " s ".") - (holes-replace-string-by-holes-backward p) - (goto-char p)) - (insert mods " " s " " typkind " #.\n#\nEnd " s ".") - (holes-replace-string-by-holes-backward p) - (goto-char p) - (holes-set-point-next-hole-destroy)))) + (insert mods " " s ".\n") + (let ((pt (point))) + (insert "\nEnd " s ".") + (goto-char pt))) + (insert mods " " s " " typkind ".\n") + (let ((pt (point))) + (insert "\nEnd " s ".") + (goto-char pt))))) (defconst reqkinds-kinds-table '(("Require Import") ("Require Export") ("Require") ("Import")) @@ -2891,6 +2900,20 @@ Used for automatic insertion of \"Proof using\" annotations.") ;; (proof-assert-next-command-interactive)))) + +(defun coq-replace-branch-with-yas-holes (s) + "replace occurrences of RE in by REPi in s. i is incremented at each replacement." + (let ((res s) (i 2)) + (setq res (replace-regexp-in-string "\\`match #" "match $1" res)) + (while (string-match "=> *\n" res nil t) + (setq res (replace-regexp-in-string ;; the regexp is made to match only + ;; the fiorst occurrence + "\\(?1:=> *\n\\)\\(.\\|\n\\)*\\'" + (concat "=> $" (int-to-string i) "\n") + res nil nil 1)) + (setq i (+ 1 i))) + res)) + (defun coq-get-goal-names (show-existentials-output) "Return the list of goal names by parsing SHOW-EXISTENTIALS-OUTPUT. @@ -2916,13 +2939,13 @@ Goals that are marked as \"only printing\" are ignored." ;; NOTE: Adding braces would be great, but it messes up indentation. (format-selector (lambda (name) (format "[%s]: #." name))) (goal-selectors (cl-mapcar format-selector goal-names)) - (snippet (string-join goal-selectors "\n"))) + (snippet (string-join goal-selectors "\n")) + (snippet (coq-insert-template snippet))) (message "%s" goal-names) (if (equal goal-selectors nil) (error "Couldn't find any named goals") (let ((start (point))) - (insert snippet) - (holes-replace-string-by-holes-backward-jump start))))))) + (if coq-use-yasnippet (yas-expand-snippet snippet) (insert snippet)))))))) (defun coq-insert-match () "Insert a match expression from a type name by Show Match. @@ -2933,14 +2956,20 @@ Also insert holes at insertion positions." (let* ((cmd)) (setq cmd (read-string "Build match for type: ")) (let* ((thematch - (proof-shell-invisible-cmd-get-result (concat "Show Match " cmd "."))) - (match (replace-regexp-in-string "=> *\n" "=> #\n" thematch))) + (proof-shell-invisible-cmd-get-result (concat "Show Match " cmd "."))) + (yasmatch (coq-replace-branch-with-yas-holes thematch))) ;; if error, it will be displayed in response buffer (see def of ;; proof-shell-invisible-cmd-get-result), otherwise: - (unless (proof-string-match coq-error-regexp match) - (let ((start (point))) - (insert match) - (holes-replace-string-by-holes-backward-jump start)))))) + (unless (proof-string-match coq-error-regexp thematch) + (if (and coq-use-yasnippet (fboundp 'yas-expand-snippet)) + (yas-expand-snippet yasmatch) + (let ((start (point))) + (insert thematch) + (indent-region start (point) nil) + (goto-char start) + (search-forward "#") + (delete-char -1))))))) + (defun coq-insert-solve-tactic () "Ask for a closing tactic name, with completion, and insert at point. diff --git a/lib/holes.el b/lib/holes.el deleted file mode 100644 index 8373cfa23..000000000 --- a/lib/holes.el +++ /dev/null @@ -1,756 +0,0 @@ -;;; holes.el --- a little piece of elisp to define holes in your buffer -*- lexical-binding:t -*- - -;; This file is part of Proof General. - -;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003-2021 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 - -;; This file uses spans, an interface for extent (XEmacs) and overlays -;; (emacs), by Healfdene Goguen for the proofgeneral mode. -;; -;; Credits also to Stefan Monnier for great help in making this file -;; cleaner. -;; -;; Further cleanups by David Aspinall. - -;; This software is free software; you can redistribute it and/or -;; modify it under the terms of the GNU General Public -;; License version 3 or later, as published by the Free Software Foundation. -;; -;; This software is distributed in the hope that it will be useful, -;; but WITHOUT ANY WARRANTY; without even the implied warranty of -;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. -;; -;; See the GNU General Public License for more details -;; (enclosed in the file COPYING). - -;;; Commentary: -;; -;; See documentation in variable holes-short-doc. -;; -;; See documentation of `holes-mode'. - -;;; Code: -(require 'span) -(eval-when-compile (require 'cl-lib)) - -;;; -;;; initialization -;;; - -(defvar holes-default-hole - (let ((ol (make-overlay 0 0))) - (delete-overlay ol) ol) - "An empty detached hole used as the default hole. -You should not use this variable.") - -(defvar holes-active-hole holes-default-hole - "The current active hole. -There can be only one active hole at a time, -and this is this one. This is not buffer local.") - - -;;; -;;; Customizable -;;; - -(defgroup holes nil - "Customization for Holes minor mode." - :prefix "holes-" - :group 'editing) - -(defcustom holes-empty-hole-string "#" - "String to be inserted for empty hole (don't put an empty string)." - :type 'string) - -(defcustom holes-empty-hole-regexp "#\\|@{\\([^{}]*\\)}" - "Regexp denoting a hole in abbrevs. -Subgroup 1 is treated specially: if it matches, it is assumed that -everything before it and after it in the regexp matches delimiters -which should be removed when making the text into a hole." - :type 'regexp) - - -;(defcustom holes-search-limit 1000 -; "Number of chars to look forward when looking for the next hole, unused for now.") -;unused for the moment - -;; The following is customizable by a command of the form: -;;for dark background -;;(custom-set-faces -;; '(holes-active-hole-face -;; ((((type x) (class color) (background light)) -;; (:background "paleVioletRed"))) -;; ) -;; ) - -(defface active-hole-face - '((((class grayscale) (background light)) :background "dimgrey") - (((class grayscale) (background dark)) :background "LightGray") - (((class color) (background dark)) - :background "darkred" :foreground "white") - (((class color) (background light)) - :background "paleVioletRed" :foreground "black")) - "Font Lock face used to highlight the active hole.") - -(defface inactive-hole-face - '((((class grayscale) (background light)) :background "lightgrey") - (((class grayscale) (background dark)) :background "Grey") - (((class color) (background dark)) - :background "mediumblue" :foreground "white") - (((class color) (background light)) - :background "lightsteelblue" :foreground "black")) - "Font Lock face used to highlight the active hole.") - -;;; -;;; Keymaps -;;; - -(defvar hole-map - (let ((map (make-sparse-keymap))) - (define-key map [(mouse-1)] #'holes-mouse-set-active-hole) - (define-key map [(mouse-3)] #'holes-mouse-destroy-hole) - (define-key map [(mouse-2)] #'holes-mouse-forget-hole) - map) - "Keymap to use on the holes's overlays. -This keymap is used only when point is on a hole. -See `holes-mode-map' for the keymap of `holes-mode'.") - -(defvar holes-mode-map - (let ((map (make-sparse-keymap))) - (define-key map [(control c) (h)] #'holes-set-make-active-hole) - (define-key map [(control c) (control y)] - #'holes-replace-update-active-hole) - (define-key map [(control meta down-mouse-1)] - #'holes-mouse-set-make-active-hole) - (define-key map [(control meta shift down-mouse-1)] - #'holes-mouse-replace-active-hole) - (define-key map [(control c) (control j)] - #'holes-set-point-next-hole-destroy) - map) - "Keymap of `holes-mode'. - -This one is active whenever we are on a buffer where `holes-mode' is active. - -This is not the keymap used on holes's overlay (see `hole-map' instead).") - -(easy-menu-define nil (list holes-mode-map) - "Menu used in Holes minor mode." - '("Holes" - ;; da: I tidied this menu a bit. I personally think this "trick" - ;; of inserting strings to add documentation looks like a real - ;; mess in menus ... I've removed it for the three below since - ;; the docs below appear in popup in messages anyway. - ;; - ;; "Make a hole active click on it" - ;; "Disable a hole click on it (button 2)" - ;; "Destroy a hole click on it (button 3)" - ["Make Hole At Point" holes-set-make-active-hole t] - ["Make Selection A Hole" holes-set-make-active-hole t] - ["Replace Active Hole By Selection" holes-replace-update-active-hole t] - ["Jump To Active Hole" holes-set-point-next-hole-destroy t] - ["Forget All Holes" holes-clear-all-buffer-holes t] - ;; look a bit better at the bottom - "---" - ["About Holes" holes-show-doc t] - "Hint: make hole with mouse: C-M-select" - "Hint: replace hole with mouse: C-M-Shift-select" - )) - - - -;;; -;;; Utility functions -;;; - -(defun holes-region-beginning-or-nil () - "Return the beginning of the acitve region, or nil." - (and mark-active (region-beginning))) - -(defun holes-region-end-or-nil () - "Return the end of the acitve region, or nil." - (and mark-active (region-end))) - -(defun holes-copy-active-region () - "Copy and retuurn the active region." - (cl-assert mark-active nil "the region is not active now.") - (copy-region-as-kill (region-beginning) (region-end)) - (car kill-ring)) - -(defun holes-is-hole-p (span) - "Non-nil if SPAN is a HOLE." - (span-property span 'hole)) - -(defun holes-hole-start-position (hole) - "Return start position of HOLE." - (cl-assert (holes-is-hole-p hole) t - "holes-hole-start-position: %s is not a hole") - (span-start hole)) - -(defun holes-hole-end-position (hole) - "Return end position of HOLE." - (cl-assert (holes-is-hole-p hole) t "holes-hole-end-position: %s is not a hole") - (span-end hole)) - -(defun holes-hole-buffer (hole) - "Return the buffer of HOLE." - "Internal." - (cl-assert (holes-is-hole-p hole) t "holes-hole-buffer: %s is not a hole") - (span-buffer hole)) - -(defun holes-hole-at (&optional pos) - "Return the hole (a span) at POS in current buffer. -If pos is not in a hole raises an error." - (span-at (or pos (point)) 'hole)) - -(defun holes-active-hole-exist-p () - "Return t if the active hole exists and is not empty (ie detached). -Use this to know if the active hole is set and usable (don't use the -active-hole-marker variable)." - (not (span-detached-p holes-active-hole))) - - -(defun holes-active-hole-start-position () - "Return the position of the start of the active hole. -See `active-hole-buffer' to get its buffer. Returns an error if -active hole doesn't exist (the marker is set to nothing)." - (cl-assert (holes-active-hole-exist-p) t - "holes-active-hole-start-position: no active hole") - (holes-hole-start-position holes-active-hole)) - -(defun holes-active-hole-end-position () - "Return the position of the start of the active hole. -See `active-hole-buffer' to get its buffer. Returns an error if -active hole doesn't exist (the marker is set to nothing)." - (cl-assert (holes-active-hole-exist-p) t - "holes-active-hole-end-position: no active hole") - (holes-hole-end-position holes-active-hole)) - - -(defun holes-active-hole-buffer () - "Return the buffer containing the active hole. -Raise an error if the active hole is not set. Don't care if the -active hole is empty." - (cl-assert (holes-active-hole-exist-p) t - "holes-active-hole-buffer: no active hole") - (holes-hole-buffer holes-active-hole)) - -(defun holes-goto-active-hole () - "Set point to active hole. -Raises an error if active-hole is not set." - (interactive) - (cl-assert (holes-active-hole-exist-p) t - "holes-goto-active-hole: no active hole") - (goto-char (holes-active-hole-start-position))) - - -(defun holes-highlight-hole-as-active (hole) - "Highlight a HOLE with the `active-hole-face'. -DON'T USE this as it would break synchronization (non active hole -highlighted)." - (cl-assert (holes-is-hole-p hole) t - "holes-highlight-hole-as-active: %s is not a hole") - (set-span-face hole 'active-hole-face)) - -(defun holes-highlight-hole (hole) - "Highlight a HOLE with the not active face. -DON'T USE this as it would break synchronization (active hole non -highlighted)." - (cl-assert (holes-is-hole-p hole) t - "holes-highlight-hole: %s is not a hole") - (set-span-face hole 'inactive-hole-face)) - -(defun holes-disable-active-hole () - "Disable the active hole. -The goal remains but is not the active one anymore. Does nothing if -the active hole is already disable." - (if (not (holes-active-hole-exist-p)) - () - ;; HACK: normal hole color, this way undo will show this hole - ;; normally and not as active hole. Ideally, undo should restore - ;; the active hole, but it doesn't, so we put the 'not active' - ;; color. - (holes-highlight-hole holes-active-hole) - (setq holes-active-hole holes-default-hole))) - -(defun holes-set-active-hole (hole) - "Set active hole to HOLE. -Error if HOLE is not a hole." - (cl-assert (holes-is-hole-p hole) t - "holes-set-active-hole: %s is not a hole") - (if (holes-active-hole-exist-p) - (holes-highlight-hole holes-active-hole)) - (setq holes-active-hole hole) - (holes-highlight-hole-as-active holes-active-hole)) - -(defun holes-is-in-hole-p (&optional pos) - "Return non-nil if POS (default: point) is in a hole, nil otherwise." - (holes-hole-at pos)) - -(defun holes-make-hole (start end) - "Make and return an (span) hole from START to END." - (let ((ext (span-make start end))) - (set-span-properties - ext `(hole t - mouse-face highlight - priority 100 ;; what should I put here? I want big priority - face secondary-selection - start-open nil - end-open t - duplicable t - evaporate t ;; really disappear if empty - ;; pointer frame-icon-glyph - keymap ,hole-map - help-echo "this is a \"hole\", button 2 to forget, button 3 to destroy, button 1 to make active" - 'balloon-help "this is a \"hole\", button 2 to forget, button 3 to destroy, button 1 to make active")) - ext)) - -(defun holes-make-hole-at (&optional start end) - "Make a hole from START to END. -If no arg default hole after point. If only one arg: error. Return -the span." - (interactive) - (let* ((rstart (or start (holes-region-beginning-or-nil) (point))) - (rend (or end (holes-region-end-or-nil) (point)))) - (if (eq rstart rend) - (progn - (goto-char rstart) - (insert holes-empty-hole-string) - (setq rend (point)))) - (holes-make-hole rstart rend))) - -(defun holes-clear-hole (hole) - "Clear the HOLE." - (cl-assert (holes-is-hole-p hole) t - "holes-clear-hole: %s is not a hole") - (if (and (holes-active-hole-exist-p) - (eq holes-active-hole hole)) - (holes-disable-active-hole)) - (span-delete hole)) - -(defun holes-clear-hole-at (&optional pos) - "Clear hole at POS (default=point)." - (interactive) - (if (not (holes-is-in-hole-p (or pos (point)))) - (error "Holes-clear-hole-at: no hole here")) - (holes-clear-hole (holes-hole-at (or pos (point))))) - - -(defun holes-map-holes (function &optional buffer from to) - "Map function FUNCTION across holes in buffer BUFFER. -Operate between character positions FROM and TO." - (fold-spans function buffer from to nil nil 'hole)) - -(defun holes-clear-all-buffer-holes (&optional start end) - "Clear all holes leaving their contents. -Operate betwenn START and END if non nil." - (interactive) - (holes-disable-active-hole) - (span-mapcar-spans - 'holes-clear-hole (or start (point-min)) (or end (point-max)) - 'hole)) - -;; limit ? -(defun holes-next (pos buffer) - "Return the first hole after POS in BUFFER. -Or after the hole at pos if there is one (default pos=point). If no -hole found, return nil." - (holes-map-holes - (lambda (h _) (and (holes-is-hole-p h) h)) buffer pos)) - -(defun holes-next-after-active-hole () - "Internal." - (cl-assert (holes-active-hole-exist-p) t - "next-active-hole: no active hole") - (holes-next (holes-active-hole-end-position) - (holes-active-hole-buffer))) - -(defun holes-set-active-hole-next (&optional buffer pos) - "Set the active hole in BUFFER to the first hole after POS. -Default pos = point and buffer = current." - (interactive) - (let ((nxthole (holes-next (or pos (point)) - (or buffer (current-buffer))))) - (if nxthole - (holes-set-active-hole nxthole) - (holes-disable-active-hole)))) - -;;;(defun holes-set-active-hole-next-after-active () -;; "sets the active hole to the first hole after active -;; hole.";;;; - -;;; (interactive) -;; (holes-next-after-active-hole) -;;) - - -(defun holes-replace-segment (start end str &optional buffer) - "Erase chars between START and END, and replace them with STR. -Operate in buffer BUFFER." - (with-current-buffer (or buffer (current-buffer)) - (goto-char end) - ;; Insert before deleting, so the markers at `start' and `end' - ;; don't get mixed up together. - (insert str) - (delete-region start end))) - -(defun holes-replace (str &optional thehole) - "Replace the current hole by STR, replace THEHOLE instead if given. -Do not use this, it breaks the right colorization of the active -goal(FIXME?). Use `replace-active-hole' instead." - (if (and (not thehole) - (not (holes-active-hole-exist-p))) - (error "No hole to fill") - ;; defensive: replacing the hole should make it detached and - ;; therefore inexistent. other reason: this is a hack: unhighlight - ;; so that undo wont show it highlighted) - (if (and (holes-active-hole-exist-p) - thehole - (eq holes-active-hole thehole)) - (holes-disable-active-hole) - ) - (let ((exthole (or thehole holes-active-hole))) - (holes-replace-segment (holes-hole-start-position exthole) - (holes-hole-end-position exthole) - (or str (car kill-ring)) ;kill ring? - (span-buffer exthole) - ) - (span-detach exthole) ;; this seems necessary for span overlays, - ;; where the buffer attached to the span is not removed - ;; automatically by the fact that the span is removed from the - ;; buffer (holes-replace-segment should perhaps take care of - ;; that) - ))) - -(defun holes-replace-active-hole (&optional str) - "Replace the active hole by STR, if no str is given, then put the selection instead." - (if (not (holes-active-hole-exist-p)) nil - (holes-replace - (or str (current-kill 0) (error "Nothing to put in hole")) - holes-active-hole))) - -(defun holes-replace-update-active-hole (&optional str) - "Replace the active hole by STR. -Like `holes-replace-active-hole', but then sets the active hole to the -following hole if it exists." - (interactive) - (cl-assert (holes-active-hole-exist-p) t - "holes-replace-update-active-hole: no active hole") - (if (holes-active-hole-exist-p) - (let ((nxthole (holes-next-after-active-hole))) - (holes-replace-active-hole - (or str - (and mark-active - (holes-copy-active-region)) - (current-kill 0) - (error "Nothing to put in hole"))) - (if nxthole (holes-set-active-hole nxthole) - (setq holes-active-hole holes-default-hole))))) - -(defun holes-delete-update-active-hole () - "Deletes the active hole and supresses its content. -Sets `holes-active-hole' to the next hole if it exists." - (interactive) - (holes-replace-update-active-hole "")) - - -;;;###autoload -(defun holes-set-make-active-hole (&optional start end) - "Make a new hole between START and END or at point, and make it active." - - (interactive) - (holes-set-active-hole (holes-make-hole-at start end))) - - -;; mouse stuff, I want to make something close to `mouse-track-insert' -;; of XEmacs, but with modifier ctrl-meta and ctrl-meta-shift - -;; Emacs and XEmacs have different ways of dealing with mouse -;; selection, but `mouse-track'(XEmacs) mouse-drag-region(Emacs) -;; have nearly the same meaning for me. So I define this -;; track-mouse-selection. - -(defalias 'holes-track-mouse-selection #'mouse-drag-track) -(defsubst holes-track-mouse-clicks () - "See `mouse-track-click-count'." - (+ mouse-selection-click-count 1)) - -(defun holes-mouse-replace-active-hole (event) - "Replace the active hole with one under mouse EVENT." - (interactive "*e") - (holes-track-mouse-selection event) - (save-excursion - ;;HACK: nothing if one click (but a second is perhaps coming) - (if (and (eq (holes-track-mouse-clicks) 1) - (not mark-active)) - () - (if (not mark-active) - (error "Nothing to put in hole") - (holes-replace-update-active-hole (current-kill 0)) - (message "hole replaced"))))) - -(defun holes-destroy-hole (&optional span) - "Destroy the hole SPAN." - (interactive) - (let* ((sp (or span (holes-hole-at (point)) - (error "No hole to destroy")))) - (save-excursion - (if (and (holes-active-hole-exist-p) - (eq sp holes-active-hole)) - (holes-disable-active-hole)) - (holes-replace "" sp) - (span-detach sp)) - (message "hole killed"))) - - -(defsubst holes-hole-at-event (event) - "Return the hole at EVENT." - (span-at-event event 'hole)) - -(defun holes-mouse-destroy-hole (event) - "Destroy the hole at EVENT." - (interactive "*e") - (holes-destroy-hole (holes-hole-at-event event))) - -;;;(span-at-event EVENT &optional PROPERTY BEFORE AT-FLAG) -;;comprend pas?? -(defun holes-mouse-forget-hole (event) - "Delete and deactivate the hole at EVENT." - (interactive "*e") - (save-excursion - (let ((ext (holes-hole-at-event event))) - (if (eq ext holes-active-hole) - (holes-disable-active-hole)) - (span-detach ext))) - (message "hole deleted")) - -(defun holes-mouse-set-make-active-hole (event) - "Make a new hole at EVENT click activate it." - (interactive "*e") - (holes-track-mouse-selection event) - - (if (and (eq (holes-track-mouse-clicks) 1) - (not mark-active)) - (holes-set-make-active-hole (point) (point)) - - (if mark-active - (holes-set-make-active-hole) - (let ((ext (holes-hole-at-event event))) - (if (and ext (holes-is-hole-p ext)) - (error "Already a hole here") - (holes-set-active-hole (holes-make-hole-at))))))) - -(defun holes-mouse-set-active-hole (event) - "Make the hole at EVENT click active." - (interactive "*e") - (let ((ext (holes-hole-at-event event))) - (if (and ext (holes-is-hole-p ext)) - (holes-set-active-hole ext) - (error "No hole here")))) - - -(defun holes-set-point-next-hole-destroy () - "Move the point to current active hole (if any and if in current buffer). -Destroy it and makes the next hole active if any." - (interactive) - (cl-assert (holes-active-hole-exist-p) nil "no active hole") - (cl-assert (eq (current-buffer) (holes-active-hole-buffer)) nil - "active hole not in this buffer") - (holes-goto-active-hole) - (holes-delete-update-active-hole)) - - -;; utilities to be used in conjunction with abbrevs. -;; The idea is to put abbrevs of the form: -;;(define-abbrev-table 'tuareg-mode-abbrev-table -;; '( -;; ("l" "let # = # in" replace-#-after-abbrev2 0) -;; ) -;; ) -;; where replace-#-after-abbrev2 should be a function which replace the -;; two #'s (two occurences going backward from abbrev expantion point) -;; by holes and leave point at the first # (deleting -;; it). holes-set-point-next-hole-destroy allow to go to the next hole. - -;;following function allow to replace occurrences of a string by a -;;hole. - -(defun holes-replace-string-by-holes-backward (limit) - "Change each occurrence of REGEXP into a hole. -Sets the active hole to the last created hole and unsets it if no hole is -created. Return the number of holes created. -The LIMIT argument bounds the search; it is a buffer position. - The match found must not begin before that position. A value of nil - means search to the beginning of the accessible portion of the buffer." - (holes-disable-active-hole) - (let ((n 0)) - (save-excursion - (while (re-search-backward holes-empty-hole-regexp limit t) - (cl-incf n) - (if (not (match-end 1)) - (holes-make-hole (match-beginning 0) (match-end 0)) - (holes-make-hole (match-beginning 1) (match-end 1)) - ;; delete end first to avoid shifting of marks - (delete-region (match-end 1) (match-end 0)) - (delete-region (match-beginning 0) (match-beginning 1))) - (holes-set-active-hole-next))) - n)) - -(defun holes-skeleton-end-hook () - "Default hook after a skeleton insertion: put holes at each interesting position." - ;; Not all versions of skeleton provide `skeleton-positions' and the - ;; corresponding @ operation :-( - (when (boundp 'skeleton-positions) - (dolist (pos skeleton-positions) ;; put holes here - (holes-set-make-active-hole pos pos)))) - -(defconst holes-jump-doc - (concat "Hit \\[holes-set-point-next-hole-destroy] to jump " - "to active hole. C-h v holes-doc to see holes doc.") - "Shortcut reminder string for jumping to active hole.") - - - -(defun holes-replace-string-by-holes-backward-jump (pos &optional noindent alwaysjump) - "Put holes between POS and point, backward, indenting. -\"#\" and \"@{..}\" between this positions will become holes. -If NOINDENT is non-nil, skip the indenting step. -If ALWAYSJUMP is non-nil, jump to the first hole even if more than one." - (unless noindent (save-excursion (indent-region pos (point)))) - (let ((n (holes-replace-string-by-holes-backward pos))) - (pcase n - (`0 nil) ; no hole, stay here. - (`1 - (goto-char pos) - (holes-set-point-next-hole-destroy)) ; if only one hole, go to it. - (_ - (goto-char pos) - (when alwaysjump (holes-set-point-next-hole-destroy)) - (unless (active-minibuffer-window) ; otherwise minibuffer gets hidden - (message (substitute-command-keys - "\\[holes-set-point-next-hole-destroy] to jump to active hole. \\[holes-show-doc] to see holes doc."))))))) - - -;;;###autoload -(define-minor-mode holes-mode - "Toggle Holes minor mode. -With arg, turn Outline minor mode on if arg is positive, off otherwise. - -The mode `holes-mode' is meant to help program editing. It is -useful to build complicated expressions by copy pasting several -peices of text from different parts of a buffer (or even from -different buffers). - -HOLES - -A hole is a piece of (highlighted) text that may be replaced by -another part of text later. There is no information stored on the -file for holes, so you can save and modify files containing holes with -no harm... You can even insert or delete characters inside holes like -any other characters. - -USE - -At any time only one particular hole, called \"active\", can be -\"filled\". Holes can be in several buffers but there is always one or -zero active hole globally. It is highlighted with a different color. - -Functions described below have default shortcuts when `holes-mode' is -on that you can customize. - -TO DEFINE A HOLE, two methods: - - o Select a region with keyboard or mouse, then use - \\[holes-set-make-active-hole]. If the selected region is empty, - then a hole containing # is created at point. - - o Select text with mouse while pressing ctrl and meta (`C-M-select'). - If the selected region is empty (i.e. if you just click while - pressing ctrl+meta), then a hole containing # is created. - -TO ACTIVATE A HOLE, click on it with the button 1 of your mouse. The -previous active hole will be deactivated. - -TO FORGET A HOLE without deleting its text, click on it with the -button 2 (middle) of your mouse. - -TO DESTROY A HOLE and delete its text, click on it with the button 3 -of your mouse. - -TO FILL A HOLE with a text selection, first make sure it is active, -then two methods: - - o Select text with keyboard or mouse and hit - \\[holes-replace-update-active-hole] - - o Select text with mouse while pressing ctrl, meta and shift - (`C-M-S-select'). This is a - generalization of the `mouse-track-insert' feature of XEmacs. This - method allows you to fill different holes faster than with the usual - copy-paste method. - -After replacement the next hole is automatically made active so you -can fill it immediately by hitting again -\\[holes-replace-update-active-hole] or `C-M-S-select'. - -TO JUMP TO THE ACTIVE HOLE, just hit -\\[holes-set-point-next-hole-destroy]. You must -be in the buffer containing the active hole. the point will move to -the active hole, and the active hole will be destroyed so you can type -something to put at its place. The following hole is automatically -made active, so you can hit \\[holes-set-point-next-hole-destroy] -again. - -It is useful in combination with abbreviations. For example in -`coq-mode' \"fix\" is an abbreviation for Fixpoint # (# : #) {struct #} : -# := #, where each # is a hole. Then hitting -\\[holes-set-point-next-hole-destroy] goes from one hole to the -following and you can fill-in each hole very quickly. - -COMBINING HOLES AND SKELETONS - -`holes' minor mode is made to work with minor mode `skeleton' minor -mode. - -KNOWN BUGS - - o Don't try to make overlapping holes, it doesn't work. (what would -it mean anyway?) - - o Cutting or pasting a hole will not produce new holes, and -undoing on holes cannot make holes re-appear." - :lighter " Holes" - (if holes-mode - (add-hook 'skeleton-end-hook #'holes-skeleton-end-hook nil t) - (remove-hook 'skeleton-end-hook #'holes-skeleton-end-hook t) - (holes-clear-all-buffer-holes))) - -;;;###autoload -(defun holes-abbrev-complete () - "Complete abbrev by putting holes and indenting. -Moves point at beginning of expanded text. Put this function as -call-back for your abbrevs, and just expanded \"#\" and \"@{..}\" will -become holes." - (if holes-mode - (holes-replace-string-by-holes-backward-jump last-abbrev-location))) - - -;;;###autoload -(defun holes-insert-and-expand (s) - "Insert S, expand it and replace #s and @{]s by holes." - ;; insert the expansion of abbrev s, and replace #s by holes. It was - ;; possible to implement it with a simple ((insert s) (expand-abbrev)) - ;; but undo would show the 2 steps, which is bad. - (let ((pos (point)) - (ins (abbrev-expansion s))) - (insert (or ins s)) - (setq last-abbrev-location pos) - (holes-abbrev-complete))) - -(provide 'holes) - -;;; holes.el ends here