Skip to content

Commit 649f8f0

Browse files
MatafouMatafou
authored
Merge pull request #862 from Matafou/removing-holes
Removing holes.el from PG.
2 parents 6946aa5 + be3339f commit 649f8f0

File tree

7 files changed

+189
-821
lines changed

7 files changed

+189
-821
lines changed

‎CHANGES‎

Lines changed: 13 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,19 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
6060
`coq-run-completely-silent' to switch back to old behavior. Note
6161
that external proof tree display is only supported if Coq/Rocq
6262
runs completely silent.
63-
63+
*** `Holes` library removed.
64+
This was a poor man's code template insertion. This is now removed
65+
and see next point below for a replacement.
66+
*** yasnippets default code templates
67+
- if you use company-coq, this is disabled by default because
68+
company-coq uses its own yasnippet templates.
69+
- Templates are defined from coq-syntax.el definitions. No
70+
exhaustivity garanteed.
71+
- You might want to define your own templates instead.
72+
- To opt out from default templates:
73+
(setq coq-yasnippet-use-default-templates nil)
74+
- To out out from yasnippet with proofgeneral:
75+
(setq coq-use-yasnippet nil)
6476

6577
* Changes of Proof General 4.5 from Proof General 4.4
6678

‎coq/coq-abbrev.el‎

Lines changed: 57 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,21 @@
2222
(require 'proof)
2323
(require 'coq-syntax)
2424

25-
(defun holes-show-doc ()
26-
(interactive)
27-
(describe-function 'holes-mode))
25+
(defcustom coq-use-yasnippet (and (not (member 'company-coq-mode coq-mode-hook))
26+
(fboundp 'yas-expand))
27+
"Should Coq use yasnippets templates.
28+
29+
Default value is t unless yasnippet is not installed or company-coq
30+
appears in the hoocoq-mode-hook."
31+
:type 'boolean
32+
:group 'coq)
33+
34+
(defcustom coq-yasnippet-use-default-templates t
35+
"Should Proofgeneral coq mode use its yasnippets default templates.
36+
37+
Set this to nil if you don't want the default yasnippets templates."
38+
:type 'boolean
39+
:group 'coq)
2840

2941
(defun coq-local-vars-list-show-doc ()
3042
(interactive)
@@ -64,10 +76,51 @@
6476
(defconst coq-terms-abbrev-table
6577
(coq-build-abbrev-table-from-db coq-terms-db))
6678

79+
(defun coq-define-yasnippets-from-db ()
80+
"Register yas snippets from default proofgeneral coq db.
81+
82+
yassnippet is a framework for inserting code templates for emacs. This
83+
will add hundreds of yas snippets, generated from proofgeneral list of
84+
coq commands (which is not necessarily always up to date). You probably
85+
want to use your own set of snippets at some point but it is a good
86+
start."
87+
(when (fboundp 'yas-define-snippets)
88+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-tactics-db))
89+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-solve-tactics-db))
90+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-solve-cheat-tactics-db))
91+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-tacticals-db))
92+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-decl-db))
93+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-defn-db))
94+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-goal-starters-db))
95+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-queries-commands-db))
96+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-other-commands-db))
97+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-ssreflect-commands-db))
98+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-terms-db))
99+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-user-tactics-db))
100+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-user-commands-db))
101+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-user-tacticals-db))
102+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-user-solve-tactics-db))
103+
(yas-define-snippets 'coq-mode (coq-yas-snippet-table-from-db coq-user-cheat-tactics-db))))
104+
105+
106+
;; this is the function called by insertion menus. TODO: separate
107+
;; these menus from yasnippet templates because this should work even
108+
;; if the user has its own templates instead of the default ones.
109+
(defun coq-insert-template (snippet)
110+
"Expand template ABBR using (by priority) yasnippet, abbrev or just ALT."
111+
(when snippet
112+
(if (and coq-use-yasnippet (fboundp 'yas-expand))
113+
(yas-expand-snippet (coq-yas-snippet-from-db snippet))
114+
(insert (coq-simple-abbrev-from-db snippet)))))
115+
116+
;; (if (fboundp 'with-undo-amalgamate) ;; emacs > 29.1
117+
;; (with-undo-amalgamate (insert abbr) (yas-expand))
118+
;; (progn (insert abbr) (yas-expand)))
119+
120+
67121

68122

69123
;;; The abbrev table built from keywords tables
70-
;#s and @{..} are replaced by holes by holes-abbrev-complete
71124
(define-abbrev-table 'coq-mode-abbrev-table
72125
(append coq-tactics-abbrev-table coq-tacticals-abbrev-table
73126
coq-commands-abbrev-table coq-terms-abbrev-table)

‎coq/coq-db.el‎

Lines changed: 49 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,6 @@
2525

2626
(eval-when-compile (require 'cl-lib)) ;decf
2727

28-
(require 'holes)
2928
(require 'diff-mode)
3029

3130
(defconst coq-syntax-db nil
@@ -88,7 +87,8 @@ the first hole even if more than one."
8887
(pt (point)))
8988
(if f (funcall f) ; call f if present
9089
(insert (or s tac)) ; insert completion and indent otherwise
91-
(holes-replace-string-by-holes-backward-jump pt nil alwaysjump)
90+
;; FIXHOLE
91+
;;(holes-replace-string-by-holes-backward-jump pt nil alwaysjump)
9292
(indent-according-to-mode))))
9393

9494

@@ -184,15 +184,16 @@ of the largest line in the menu (without abbrev and shortcut specifications).
184184
Used by `coq-build-menu-from-db', which you should probably use instead. See
185185
`coq-syntax-db' for DB structure."
186186
(let ((l db) (res ()) (size lgth)
187-
(keybind-abbrev (substitute-command-keys " \\[expand-abbrev]")))
187+
(keybind-abbrev (if coq-use-yasnippet (substitute-command-keys " \\[yas-expand]")
188+
(substitute-command-keys " \\[expand-abbrev]"))))
188189
(while (and l (> size 0))
189190
(let* ((hd (pop l))
190191
(menu (nth 0 hd)) ; e1 = menu entry
191192
(abbrev (nth 1 hd)) ; e2 = abbreviation
192193
(complt (nth 2 hd)) ; e3 = completion
193194
;; (state (nth 3 hd)) ; e4 = state changing
194195
;; (color (nth 4 hd)) ; e5 = colorization string
195-
(insertfn (nth 5 hd)) ; e6 = function for smart insertion
196+
;; (insertfn (nth 5 hd)) ; e6 = function for smart insertion not used
196197
(menuhide (nth 6 hd)) ; e7 = if non-nil : hide in menu
197198
(entry-with (max (- menuwidth (length menu)) 0))
198199
(spaces (make-string entry-with ? ))
@@ -205,8 +206,7 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See
205206
(concat menu
206207
(if (not abbrev) ""
207208
(concat spaces "(" abbrev keybind-abbrev ")")))
208-
;;insertion function if present otherwise insert completion
209-
(if insertfn insertfn `(holes-insert-and-expand ,complt))
209+
`(coq-insert-template ,complt)
210210
t)))
211211
(push menu-entry res)))
212212
(cl-decf size)))
@@ -250,10 +250,9 @@ structure."
250250
(setq lgth (length l)))
251251
res))
252252

253-
(defcustom coq-holes-minor-mode t
254-
"*Whether to apply holes minor mode (see `holes-show-doc') in coq mode."
255-
:type 'boolean
256-
:group 'coq)
253+
(defun coq-simple-abbrev-from-db (s)
254+
"Returns the coq db abbrevitaion string S cleaned from template markups."
255+
(if s (replace-regexp-in-string "#\\|@{\\(?1:[^{}]*\\)}" "" s)))
257256

258257
(defun coq-build-abbrev-table-from-db (db)
259258
"Take a keyword database DB and return an abbrev table.
@@ -264,12 +263,47 @@ See `coq-syntax-db' for DB structure."
264263
(_e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
265264
(e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
266265
(e3 (car tl2)) (_tl3 (cdr tl2)) ; e3 = completion
267-
)
266+
(e3clean (coq-simple-abbrev-from-db e3)))
267+
;; careful: nconc destructive!
268+
(when e2 (push `(,e2 ,e3clean nil :system t) res))
269+
(setq l tl)))
270+
(nreverse res)))
271+
272+
273+
(defun coq-db--replace-abbrev-yas (i mtch)
274+
"Translationi of a coq db abbrev spec to a yasnippet one."
275+
(cond
276+
;; FIXME: define a "end point for the snippet: that is the place where the
277+
;; cursor should go after fiolling the holes. Generally it is the place where
278+
;; you want to continue editing.
279+
((string-equal mtch "#") (concat "$" (int-to-string i)))
280+
(t (concat "${" (int-to-string i) ":" (match-string 1 mtch) "}"))
281+
)
282+
)
283+
284+
(defun coq-yas-snippet-from-db (s)
285+
"Translate the coq db abbrevitaion string S into the yasnippet abbrev format."
286+
(if s
287+
(let ((cpt 0))
288+
(replace-regexp-in-string
289+
"#\\|@{\\(?1:[^{}]*\\)}"
290+
(lambda (mtch) (setq cpt (+ 1 cpt)) (coq-db--replace-abbrev-yas cpt mtch))
291+
s))))
292+
293+
(defun coq-yas-snippet-table-from-db (db)
294+
"Take a keyword database DB and return a list of yasnippets.
295+
296+
The list contains lists or args to be given to yas-define-snippets.
297+
See `coq-syntax-db' for DB structure."
298+
(let ((l db) (res ()))
299+
(while l
300+
(let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4
301+
(e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
302+
(e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
303+
(e3 (car tl2)) (_tl3 (cdr tl2)) ; e3 = completion
304+
(yas_e3 (coq-yas-snippet-from-db e3)))
268305
;; careful: nconc destructive!
269-
(when e2
270-
(push `(,e2 ,e3 ,(if coq-holes-minor-mode #'holes-abbrev-complete)
271-
:system t)
272-
res))
306+
(when e2 (push `(,e2 ,yas_e3 ,e1) res))
273307
(setq l tl)))
274308
(nreverse res)))
275309

‎coq/coq-mode.el‎

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -235,10 +235,6 @@ Near here means PT is either inside or just aside of a comment."
235235
;; we can cope with nested comments
236236
(set (make-local-variable 'comment-quote-nested) nil)
237237

238-
;; FIXME: have abbreviation without holes
239-
;(if coq-use-editing-holes (holes-mode 1))
240-
(if (fboundp 'holes-mode) (holes-mode 1))
241-
242238
;; Setup Proof-General interface to Coq.
243239
(if coq-use-pg (coq-pg-setup))
244240

‎coq/coq-syntax.el‎

Lines changed: 21 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -251,11 +251,10 @@ so for the following reasons:
251251
("now_show" nil "now_show" t "now_show")
252252
("nra" nil "nra" t "nra")
253253
("nsatz" nil "nsatz" t "nsatz")
254-
("omega" "o" "omega" t "omega")
255254
("pattern" "pat" "pattern" t "pattern")
256255
("pattern(s)" "pats" "pattern # , #" t)
257256
("pattern at" "pata" "pattern # at #" t)
258-
("pose" "po" "pose ( # := # )" t "pose")
257+
("pose" "pose" "pose ( # := # )" t "pose")
259258
("prolog" "prol" "prolog" t "prolog")
260259
("psatz" nil "psatz" t "psatz")
261260
("quote" "quote" "quote" t "quote")
@@ -268,8 +267,8 @@ so for the following reasons:
268267
("rename into" "ren" "rename # into #" t "rename")
269268
("replace with" "rep" "replace # with #" t "replace")
270269
("replace with in" "repi" "replace # with # in #" t)
271-
("revert dependent" "r" "revert dependent" t "revert\\s-+dependent")
272-
("revert" "r" "revert" t "revert")
270+
("revert dependent" "rd" "revert dependent" t "revert\\s-+dependent")
271+
("revert" "rev" "revert" t "revert")
273272
("rewrite_all" nil "rewrite_all" t "rewrite_all")
274273
("rewrite_all <-" nil "rewrite_all" t "rewrite_all")
275274
("rewrite <- in" "ri<" "rewrite <- # in #" t)
@@ -320,9 +319,9 @@ so for the following reasons:
320319
("nat_norm" "nnorm" "nat_norm" t "nat_norm")
321320
("bool_congr" "bcongr" "bool_congr" t "bool_congr")
322321
("prop_congr" "prcongr" "prop_congr" t "prop_congr")
323-
("move" "m" "move" t "move")
324-
("pose" "po" "pose # := #" t "pose")
325-
("set" "set" "set # := #" t "set")
322+
("move" "mo" "move" t "move")
323+
("pose (ssr)" "po" "pose # := #" t "pose(ssr)")
324+
("set (ssr)" "se" "set # := #" t "set (ssr)")
326325
("have" "hv" "have # : #" t "have")
327326
("congr" "con" "congr #" t "congr")
328327
("wlog" "wlog" "wlog : / #" t "wlog")
@@ -499,14 +498,13 @@ so for the following reasons:
499498
("Program Instance" "pinstance" "Program Instance [ # ] => # where \n# := #;\n# := #." t "Program\\s-+Instance")
500499
("Let" "Let" "Let # : # := #." t "Let")
501500
("Local Ltac2" nil "Local Ltac2 # := #." t "Local\\s-+Ltac2")
502-
("Ltac2 Type" "lt2rty" "Ltac2 Type rec # := #." t "Ltac2 Type rec")
501+
("Ltac2 Type rec" "lt2rty" "Ltac2 Type rec # := #." t "Ltac2 Type rec")
503502
("Ltac2 Type" "lt2ty" "Ltac2 Type # := #." t "Ltac2 Type")
504-
("Ltac2 Type" "lt2oty" "Ltac2 Type # ::= #." t "Ltac2 Type")
505-
("Ltac2 Type" "lt2wty" "Ltac2 Type #." t "Ltac2 Type")
506-
("Ltac2" "lt2mr" "Ltac2 mutable rec # := #." t "Ltac2 mutable rec")
507-
("Ltac2" "lt2m" "Ltac2 mutable # := #." t "Ltac2 mutable")
508-
("Ltac2" "lt2r" "Ltac2 rec # := #." t "Ltac2 rec")
509-
("Ltac2" "lt2s" "Ltac2 Set # := #." t "Ltac2 Set")
503+
("Ltac2 Type ::=" "lt2oty" "Ltac2 Type # ::= #." t "Ltac2 Type ::=")
504+
("Ltac2 mutable rec" "lt2mr" "Ltac2 mutable rec # := #." t "Ltac2 mutable rec")
505+
("Ltac2 mutable" "lt2m" "Ltac2 mutable # := #." t "Ltac2 mutable")
506+
("Ltac2 rec" "lt2r" "Ltac2 rec # := #." t "Ltac2 rec")
507+
("Ltac2 Set" "lt2s" "Ltac2 Set # := #." t "Ltac2 Set")
510508
("Ltac2" "lt2" "Ltac2 # := #." t "Ltac2")
511509
("Local Ltac" nil "Local Ltac # := #." t "Local\\s-+Ltac")
512510
("Ltac" "ltac" "Ltac # := #." t "Ltac")
@@ -739,18 +737,19 @@ They deserve a separate menu for sending them to Coq without insertion.")
739737
("Set Maximal Implicit Insertion" nil "Set Maximal Implicit Insertion" t "Set Maximal\\s-+Implicit\\s-+Insertion")
740738
("Set Nonrecursive Elimination Schemes" nil "Set Nonrecursive Elimination Schemes" t "Set Nonrecursive\\s-+Elimination\\s-+Schemes")
741739
("Set Parsing Explicit" nil "Set Parsing Explicit" t "Set Parsing\\s-+Explicit")
740+
("Set Nested Proofs Allowed" "snpa" "Set Nested Proofs Allowed" t "Set\\s-+Nested\\s-+Proofs\\s-+Allowed")
742741
("Set Primitive Projections" nil "Set Primitive Projections" t "Set Primitive\\s-+Projections")
743-
("Set Printing All" nil "Set Printing All" t "Set\\s-+Printing\\s-+All")
744-
("Set Printing Coercions" nil "Set Printing Coercions" t "Set\\s-+Printing\\s-+Coercions")
742+
("Set Printing All" "spa" "Set Printing All" t "Set\\s-+Printing\\s-+All")
743+
("Set Printing Coercions" "spc" "Set Printing Coercions" t "Set\\s-+Printing\\s-+Coercions")
745744
("Set Printing Compact Contexts" nil "set Printing Compact Contexts" t "set\\s-+Printing\\s-+Compact\\s-+Contexts")
746745
("Set Printing Depth" nil "Set Printing Depth" t "Set\\s-+Printing\\s-+Depth")
747746
("Set Printing Existential Instances" nil "Set Printing Existential Instances" t "Set\\s-+Printing\\s-+Existential\\s-+Instances")
748747
("Set Printing Goal Tags" nil "Set Printing Goal Tags" t "Set\\s-+Printing\\s-+Goal\\s-+Tags")
749748
("Set Printing Goal Names" nil "Set Printing Goal Names" t "Set\\s-+Printing\\s-+Goal\\s-+Names")
750-
("Set Printing Implicit" nil "Set Printing Implicit" t "Set\\s-+Printing\\s-+Implicit")
749+
("Set Printing Implicit" "spi" "Set Printing Implicit" t "Set\\s-+Printing\\s-+Implicit")
751750
("Set Printing Implicit Defensive" nil "Set Printing Implicit Defensive" t "Set\\s-+Printing\\s-+Implicit\\s-+Defensive")
752751
("Set Printing Matching" nil "Set Printing Matching" t "Set\\s-+Printing\\s-+Matching")
753-
("Set Printing Notations" nil "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations")
752+
("Set Printing Notations" "spn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations")
754753
("Set Printing Primitive Projection Compatibility" nil "Set Printing Primitive Projection Compatibility" t "Set\\s-+Printing\\s-+Primitive\\s-+Projection\\s-+Compatibility")
755754
("Set Printing Primitive Projection Parameters" nil "Set Printing Primitive Projection Parameters" t "Set\\s-+Printing\\s-+Primitive\\s-+Projection\\s-+Parameters")
756755
("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.")
867866
("Unset Loose Hint Behavior" nil "Unset Loose Hint Behavior" t "Unset Loose\\s-+Hint\\s-+Behavior")
868867
("Unset Maximal Implicit Insertion" nil "Unset Maximal Implicit Insertion" t "Unset Maximal\\s-+Implicit\\s-+Insertion")
869868
("Unset Nonrecursive Elimination Schemes" nil "Unset Nonrecursive Elimination Schemes" t "Unset Nonrecursive\\s-+Elimination\\s-+Schemes")
869+
("Unset Nested Proofs Allowed" "usnpa" "Unset Nested Proofs Allowed" t "Unset\\s-+Nested\\s-+Proofs\\s-+Allowed")
870870
("Unset Parsing Explicit" nil "Unset Parsing Explicit" t "Unset Parsing\\s-+Explicit")
871871
("Unset Primitive Projections" nil "Unset Primitive Projections" t "Unset Primitive\\s-+Projections")
872-
("Unset Printing All" nil "Unset Printing All" t "Unset Printing\\s-+All")
872+
("Unset Printing All" "uspa" "Unset Printing All" t "Unset Printing\\s-+All")
873873
("Unset Printing Coercions" nil "Unset Printing Coercions" t "Unset\\s-+Printing\\s-+Coercions")
874874
("Unset Printing Compact Contexts" nil "Unset Printing Compact Contexts" t "Unset\\s-+Printing\\s-+Compact\\s-+Contexts")
875875
("Unset Printing Depth" nil "Unset Printing Depth" t "Unset Printing\\s-+Depth")
876876
("Unset Printing Existential Instances" nil "Unset Printing Existential Instances" t "Unset Printing\\s-+Existential\\s-+Instances")
877-
("Unset Printing Implicit" nil "Unset Printing Implicit" t "Unset Printing\\s-+Implicit")
877+
("Unset Printing Implicit" "uspi" "Unset Printing Implicit" t "Unset Printing\\s-+Implicit")
878878
("Unset Printing Implicit Defensive" nil "Unset Printing Implicit Defensive" t "Unset Printing\\s-+Implicit\\s-+Defensive")
879879
("Unset Printing Matching" nil "Unset Printing Matching" t "Unset Printing\\s-+Matching")
880-
("Unset Printing Notations" nil "Unset Printing Notations" t "Unset Printing\\s-+Notations")
880+
("Unset Printing Notations" "uspn" "Unset Printing Notations" t "Unset Printing\\s-+Notations")
881881
("Unset Printing Primitive Projection Compatibility" nil "Unset Printing Primitive Projection Compatibility" t "Unset Printing\\s-+Primitive\\s-+Projection\\s-+Compatibility")
882882
("Unset Printing Primitive Projection Parameters" nil "Unset Printing Primitive Projection Parameters" t "Unset Printing\\s-+Primitive\\s-+Projection\\s-+Parameters")
883883
("Unset Printing Projections" nil "Unset Printing Projections" t "Unset Printing\\s-+Projections")

0 commit comments

Comments
 (0)