Removing holes

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
 

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)

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,15 +184,16 @@ 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
 	     (abbrev   	 (nth 1 hd)) ; e2 = abbreviation
 	     (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)))
 

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))
 

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")