menu, holes and abbrev made better.

3 files changed, 116 insertions, 66 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 6d9a097e..15302aeb 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -10,28 +10,28 @@
   (define-abbrev-table 'coq-mode-abbrev-table
 	 '(
 		("a" "auto" holes-abbrev-complete 4)
-		("ar" "autorewrite [ # ] using #" holes-abbrev-complete 1)
-		("ab" "absurd #" holes-abbrev-complete 0)
-		("abs" "absurd #" holes-abbrev-complete 0)
-		("ap" "apply #" holes-abbrev-complete 16)
+		("ar" "autorewrite [ # ] using @{db}" holes-abbrev-complete 1)
+		("ab" "absurd " holes-abbrev-complete 0)
+		("abs" "absurd " holes-abbrev-complete 0)
+		("ap" "apply " holes-abbrev-complete 16)
 		("as" "assumption" holes-abbrev-complete 4)
 		("ass" "assert ( # : # )" holes-abbrev-complete 4)
 		("au" "auto" holes-abbrev-complete 1)
-		("aw" "auto with #" holes-abbrev-complete 1)
+		("aw" "auto with " holes-abbrev-complete 1)
 		("awa" "auto with arith" holes-abbrev-complete 4)
-		("c" "cases #" holes-abbrev-complete 1)
-		("ch" "change #" holes-abbrev-complete 1)
+		("c" "cases " holes-abbrev-complete 1)
+		("ch" "change " holes-abbrev-complete 1)
 		("chi" "change # in #" holes-abbrev-complete 1)
 		("chwi" "change # with # in #" holes-abbrev-complete 1)
 		("con" "constructor" holes-abbrev-complete 3)
 		("cong" "congruence" holes-abbrev-complete 3)
-		("dec" "decompose [#] #" holes-abbrev-complete 3)
+		("dec" "decompose [#] @{hyp}" holes-abbrev-complete 3)
 		("def" "Definition #:# := #." holes-abbrev-complete 5)
 		("def2" "Definition # (# : #) (# : #):# := #." holes-abbrev-complete 5)
 		("def3" "Definition # (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5)
 		("def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5)
 		("deg" "decide equality" holes-abbrev-complete 3)
-		("des" "destruct #" holes-abbrev-complete 0)
+		("des" "destruct " holes-abbrev-complete 0)
 		("desu" "destruct # using #" holes-abbrev-complete 0)
 		("desa" "destruct # as #" holes-abbrev-complete 0)
 		("dis" "discriminate" holes-abbrev-complete 0)
@@ -42,7 +42,7 @@
 		("e" "elim #" holes-abbrev-complete 1)
 		("ea" "eauto" holes-abbrev-complete 0)
 		("eap" "eapply #" holes-abbrev-complete 0)
-		("eaw" "eauto with #" holes-abbrev-complete 0)
+		("eaw" "eauto with @{db}" holes-abbrev-complete 0)
 		("eawa" "eauto with arith" holes-abbrev-complete 0)
 		("el" "elim #" holes-abbrev-complete 0)
 		("elu" "elim # using #" holes-abbrev-complete 0)
@@ -52,30 +52,30 @@
 		("f2" "fun (#:#) (#:#) => #" holes-abbrev-complete 0)
 		("f3" "fun (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0)
 		("f4" "fun (#:#) (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0)
-		("fi" "functional induction #" holes-abbrev-complete 0)
-		("fix" "Fixpoint # (#:#) {struct #} : # :=\n#." holes-abbrev-complete 3)
+		("fi" "functional induction @{f} @{args}" holes-abbrev-complete 0)
+		("fix" "Fixpoint # (#:#) {struct @{arg}} : # :=\n#." holes-abbrev-complete 3)
 		("fo" "forall #,#" holes-abbrev-complete 0)
 		("fo1" "forall #:#,#" holes-abbrev-complete 0)
 		("fo2" "forall (#:#) (#:#), #" holes-abbrev-complete 0)
 		("fo3" "forall (#:#) (#:#) (#:#), #" holes-abbrev-complete 0)
 		("fo4" "forall (#:#) (#:#) (#:#) (#:#), #" holes-abbrev-complete 0)
-		("fs" "Functional Scheme # := Induction for #." holes-abbrev-complete 0)
+		("fs" "Functional Scheme @{name} := Induction for @{fun}." holes-abbrev-complete 0)
 		("fsto" "firstorder" holes-abbrev-complete 0)
-		("fsw" "Functional Scheme # := Induction for # with #." holes-abbrev-complete 0)
+		("fsw" "Functional Scheme @{name} := Induction for @{fun} with @{mutfuns}." holes-abbrev-complete 0)
 		("g" "generalize #" holes-abbrev-complete 0)
 		("ge" "generalize #" holes-abbrev-complete 0)
 		("gen" "generalize #" holes-abbrev-complete 0)
 		("hc" "Hint Constructors # : #." holes-abbrev-complete 0)
-		("he" "Hint Extern # # => # : #." holes-abbrev-complete 0)
-		("hi" "Hint Immediate # : #." holes-abbrev-complete 0)
-		("hr" "Hint Resolve # : #." holes-abbrev-complete 0)
-		("hrw" "Hint Rewrite [#] in # using #." holes-abbrev-complete 0)
+		("he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." holes-abbrev-complete 0)
+		("hi" "Hint Immediate # : @{db}." holes-abbrev-complete 0)
+		("hr" "Hint Resolve # : @{db}." holes-abbrev-complete 0)
+		("hrw" "Hint Rewrite [#] in @{db} using @{tac}." holes-abbrev-complete 0)
 		("hs" "Hints # : #." holes-abbrev-complete 0)
 		("hu" "Hint Unfold # : #." holes-abbrev-complete 0)
-		("i" "intro #" holes-abbrev-complete 10)
+		("i" "intro " holes-abbrev-complete 10)
 		("if" "if # then # else #" holes-abbrev-complete 1)
 		("in" "intro" holes-abbrev-complete 1)
-		("inf" "infix \"#\" := # (at level #) : #." holes-abbrev-complete 1)
+		("inf" "infix \"#\" := # (at level #) : @{scope}." holes-abbrev-complete 1)
 		("ind" "induction #" holes-abbrev-complete 2)
 		("indv" "Inductive # : # := # : #." holes-abbrev-complete 0)
 		("indv2" "Inductive # : # :=\n| # : #\n| # : #." holes-abbrev-complete 0)
@@ -102,8 +102,8 @@
 		("moi2" "Module # <: #.\n#\nEnd #." holes-abbrev-complete 0)
 		("nota" "Notation \"#\" := # (at level #, # at level #)." holes-abbrev-complete 0)
 		("notas" "Notation \"#\" := # (at level #, # associativity)." holes-abbrev-complete 0)
-		("notasc" "Notation \"#\" := # (at level #, # at level #) : #." holes-abbrev-complete 0)
-		("notassc" "Notation \"#\" := # (at level #, # associativity) : #." holes-abbrev-complete 0)
+		("notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." holes-abbrev-complete 0)
+		("notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." holes-abbrev-complete 0)
 		("o" "omega" holes-abbrev-complete 0)
 		("om" "Omega" holes-abbrev-complete 0)
 		("p" "Print #" holes-abbrev-complete 3)
@@ -116,6 +116,7 @@
 		("refl" "reflexivity #" holes-abbrev-complete 0)
 		("ri" "rewrite # in #" holes-abbrev-complete 19)
 		("ril" "rewrite <- # in #" holes-abbrev-complete 0)
+		("ri<" "rewrite <- # in #" holes-abbrev-complete 0)
 		("re" "rewrite #" holes-abbrev-complete 0)
 		("re<" "rewrite <- #" holes-abbrev-complete 0)
 		("ring" "ring #" holes-abbrev-complete 19)
@@ -125,7 +126,7 @@
 		("setg" "set ( # := #) in |-*" holes-abbrev-complete 23)
 		("seti" "set ( # := #) in #" holes-abbrev-complete 23)
 		("su" "subst #" holes-abbrev-complete 23)
-		("sc" "Scheme # := Induction for # Sort #." nil 0)
+		("sc" "Scheme @{name} := Induction for # Sort #." nil 0)
 		("si" "simpl" holes-abbrev-complete 0)
 		("sp" "Split" holes-abbrev-complete 1)
 		("sy" "symmetry" holes-abbrev-complete 0)
diff --git a/coq/coq.el b/coq/coq.el
index 0886799f..3f2ecb9c 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -101,32 +101,42 @@
      ["Inductive3            indv3<C-BS>" (insert-and-expand "indv3") t]
      ["Inductive4            indv4<C-BS>" (insert-and-expand "indv4") t]
      ""
-     ["Module                mo<C-BS>" (insert-and-expand "mo") t]
-     ["Module (<:)           mo2<C-BS>" (insert-and-expand "mo") t]
-     ["Module (interactive)  moi<C-BS>" (insert-and-expand "moi") t]
-     ["Module (interactive <:) moi2<C-BS>" (insert-and-expand "moi2") t]
-     ["Module Type           mt<C-BS>" (insert-and-expand "mt") t]
-     ["Module Type (interactive) mti<C-BS>" (insert-and-expand "mti") t]
-     ["Declare Module        dm<C-BS>" (insert-and-expand "dm") t]
-     ["Declare Module (<:)   dm2<C-BS>" (insert-and-expand "dm") t]
-     ["Declare Module (inter.) dmi<C-BS>" (insert-and-expand "dmi") t]
-     ["Declare Module (inter. <:) dmi2<C-BS>" (insert-and-expand "dmi2") t]
-     ""
-     ["Scheme                sc<C-BS>" (insert-and-expand "sc") t]
-     ["Functional Scheme     fs<C-BS>" (insert-and-expand "fs") t]
-     ["Functional Scheme with    fsw<C-BS>" (insert-and-expand "fsw") t]
-     ""
-     ["Hint Constructors     hc<C-BS>" (insert-and-expand "hc") t]
-     ["Hint Immediate        hi<C-BS>" (insert-and-expand "hi") t]
-     ["Hint Resolve          hr<C-BS>" (insert-and-expand "hr") t]
-     ["Hint Rewrite          hrw<C-BS>" (insert-and-expand "hrw") t]
-     ["Hint Extern           he<C-BS>" (insert-and-expand "he") t]
-     ""
-     ["infix                 inf<C-BS>" (insert-and-expand "inf") t]     
-     ["Notation (no assoc)   nota<C-BS>" (insert-and-expand "nota") t]     
-     ["Notation (assoc)         notas<C-BS>" (insert-and-expand "notas") t]     
-     ["Notation (no assoc, scope) notasc<C-BS>" (insert-and-expand "notasc") t]     
-     ["Notation (assoc, scope) notassc<C-BS>" (insert-and-expand "notassc") t]     
+     ("Modules"
+      "COMMAND               ABBREVIATION"
+      ["Module                mo<C-BS>" (insert-and-expand "mo") t]
+      ["Module (<:)           mo2<C-BS>" (insert-and-expand "mo") t]
+      ["Module (interactive)  moi<C-BS>" (insert-and-expand "moi") t]
+      ["Module (interactive <:) moi2<C-BS>" (insert-and-expand "moi2") t]
+      ["Module Type           mt<C-BS>" (insert-and-expand "mt") t]
+      ["Module Type (interactive) mti<C-BS>" (insert-and-expand "mti") t]
+      ""
+      ["Declare Module        dm<C-BS>" (insert-and-expand "dm") t]
+      ["Declare Module (<:)   dm2<C-BS>" (insert-and-expand "dm") t]
+      ["Declare Module (inter.) dmi<C-BS>" (insert-and-expand "dmi") t]
+      ["Declare Module (inter. <:) dmi2<C-BS>" (insert-and-expand "dmi2") t]
+      )
+     ("Hints"
+      "COMMAND               ABBREVIATION"
+      ["Hint Constructors     hc<C-BS>" (insert-and-expand "hc") t]
+      ["Hint Immediate        hi<C-BS>" (insert-and-expand "hi") t]
+      ["Hint Resolve          hr<C-BS>" (insert-and-expand "hr") t]
+      ["Hint Rewrite          hrw<C-BS>" (insert-and-expand "hrw") t]
+      ["Hint Extern           he<C-BS>" (insert-and-expand "he") t]
+     )
+     ("Schemes"
+      "COMMAND               ABBREVIATION"
+      ["Scheme                sc<C-BS>" (insert-and-expand "sc") t]
+      ["Functional Scheme     fs<C-BS>" (insert-and-expand "fs") t]
+      ["Functional Scheme with    fsw<C-BS>" (insert-and-expand "fsw") t]
+      )
+     ("Notations"
+      "COMMAND               ABBREVIATION"
+      ["infix                           inf<C-BS>" (insert-and-expand "inf") t]     
+      ["Notation (no assoc)             nota<C-BS>" (insert-and-expand "nota") t]     
+      ["Notation (assoc)                notas<C-BS>" (insert-and-expand "notas") t]     
+      ["Notation (no assoc, scope)      notasc<C-BS>" (insert-and-expand "notasc") t]     
+      ["Notation (assoc, scope)         notassc<C-BS>" (insert-and-expand "notassc") t]
+      )
      )
 
     ("Insert term" 
@@ -136,13 +146,16 @@
      ["forall2       fo2<C-BS>" (insert-and-expand "fo2") t]
      ["forall3       fo3<C-BS>" (insert-and-expand "fo3") t]
      ["forall4       fo4<C-BS>" (insert-and-expand "fo4") t]
+     ""
      ["fun           f<ctrl-bacspace>"  (insert-and-expand "f") t]
      ["fun1          f1<ctrl-bacspace>"  (insert-and-expand "f1") t]
      ["fun2          f2<C-BS>" (insert-and-expand "f2") t]
      ["fun3          f3<C-BS>" (insert-and-expand "f3") t]
      ["fun4          f4<C-BS>" (insert-and-expand "f4") t]
+     ""
      ["if then else  if<C-BS>"  (insert-and-expand "li") t]
      ["let in        li<C-BS>"  (insert-and-expand "li") t]
+     ""
      ["match         m<C-BS>"  (insert-and-expand "m") t]
      ["match2        m2<C-BS>"  (insert-and-expand "m2") t]
      ["match3        m3<C-BS>"  (insert-and-expand "m3") t]
@@ -195,9 +208,9 @@
      ["reflexivity            refl<C-BS>"  (insert-and-expand "refl") t]
      ["replace                rep<C-BS>"  (insert-and-expand "rep") t]
      ["rewrite                r<C-BS>"  (insert-and-expand "r") t]
-     ["rewrite in             ri<C-BS>"  (insert-and-expand "r") t]
-     ["rewrite <-             rl<C-BS>"  (insert-and-expand "r") t]
-     ["rewrite <- in          ril<C-BS>"  (insert-and-expand "r") t]
+     ["rewrite in             ri<C-BS>"  (insert-and-expand "ri") t]
+     ["rewrite <-             r<<C-BS>"  (insert-and-expand "rl") t]
+     ["rewrite <- in          ri<<C-BS>"  (insert-and-expand "ril") t]
      ["set                    set<C-BS>"  (insert-and-expand "set") t]
      ["set in hyp             seth<C-BS>"  (insert-and-expand "seth") t]
      ["set in goal            setg<C-BS>"  (insert-and-expand "setg") t]
diff --git a/generic/holes.el b/generic/holes.el
index 4d7fe7b0..4a03f9de 100644
--- a/generic/holes.el
+++ b/generic/holes.el
@@ -151,6 +151,9 @@ is), which is annoying.
 (defcustom empty-hole-string "#"
   "string to be inserted for empty hole (don't put an empty string).")
 
+(defcustom empty-hole-regexp "#\\|\\(@{\\)\\([^{}]*\\)\\(}\\)"
+  "Regexp denoting a hole in abbrevs. Must match either `empty-hole-string' or a regexp formed by three consecutive groups (i.e. \\\\(...\\\\) )  (other groups must be shy (i.e. \\\\(?:...\\\\))), denoting the exact limits of the hole (the middle group), the opening and closing delimiters of the hole (first and third groups) which will be deleted after abbrev expand. For example: \"#\\|\\(@{\\)\\([^{}]*\\)\\(}\\)\" matches any # or @{text} but in the second case the abbrev expand will be a hole containing text without brackets.")
+
 (defcustom hole-search-limit 1000
   "number of chars to look forward when looking for the next hole, unused for now");unused for the moment
 
@@ -779,6 +782,16 @@ is), which is annoying.
 	 )
   )
 
+(defun count-re-in-string (regexp str)
+  (let ((cpt 0) (s str))
+	 (while (and (not (string-equal s "")) (string-match regexp s) )
+		(setq cpt (+ cpt 1))
+		(setq s (substring s (match-end 0)))
+		)
+	 cpt
+	 )
+  )
+
 (defun count-chars-in-last-expand ()
   (length (abbrev-expansion last-abbrev-text))
   )
@@ -803,7 +816,7 @@ end of last abbrev expansion. "
   )
 
 (defun count-holes-in-last-expand ()
-  (count-char-in-string empty-hole-string (abbrev-expansion last-abbrev-text))
+  (count-re-in-string empty-hole-regexp (abbrev-expansion last-abbrev-text))
   )
 
 (defun replace-string-by-holes (start end str)
@@ -825,7 +838,7 @@ created"
     )
   )
 
-(defun replace-string-by-holes-backward (num str)
+(defun replace-string-by-holes-backward (num regexp)
 
   "make num occurrences of str be holes looking backward. sets the
 active hole to the last created hole and unsets it if no hole is
@@ -834,13 +847,19 @@ created. return t if num is > 0, nil otherwise."
   (interactive)
   (disable-active-hole)
   (if (<= num 0) nil
-	 (let* ((n num) (lgth (length str)))
+	 (let* ((n num) (lgth 0))
 		(save-excursion
 		  (while (> n 0)
 			 (progn 
-				(search-backward str) 
-				(make-hole (point) (+ (point) lgth))
-				(set-active-hole-next)
+				(re-search-backward regexp)
+				(if (string-equal (match-string 0) empty-hole-string) 
+					 (make-hole (match-beginning 0) (match-end 0))
+				  (make-hole (match-beginning 2) (match-end 2))
+				  (goto-char (match-beginning 3))
+				  (delete-char (length (match-string 3)))
+				  (goto-char (match-beginning 1))
+				  (delete-char (length (match-string 1))))
+				  (set-active-hole-next)
 				(setq n (- n 1)))
 			 )
 		  )
@@ -861,16 +880,28 @@ created. return t if num is > 0, nil otherwise."
 
   (interactive)
   (and (replace-string-by-holes-backward num str)
-		 (set-point-next-hole-destroy))
+		 t ;(set-point-next-hole-destroy)
+		 )
   )
 
 
 
 (defun holes-abbrev-complete ()
-  "complete abbrev by putting holes and indenting."
-  (indent-last-expand)
-  (replace-string-by-holes-backward-move-point 
-	(count-holes-in-last-expand) empty-hole-string)
+  "Complete abbrev by putting holes and indenting. Moves point at beginning of expanded text."
+  (let ((pos last-abbrev-location))
+	 (indent-last-expand)
+	 (replace-string-by-holes-backward-move-point 
+	  (count-holes-in-last-expand) empty-hole-regexp)
+	 (if (> (count-holes-in-last-expand) 1) 
+		  (progn (goto-char pos)
+					(message "Hit meta-return to jump to active hole. M-x holes-short-doc to see holes documentation."))
+
+		(if (= (count-holes-in-last-expand) 0) () ; no hole, stay here.
+		  (goto-char pos)
+		  (set-point-next-hole-destroy) ; if only one hole, go to it.
+		  )
+		)
+	 )
   )
 
 ; insert the expansion of abbrev s, and replace #s by holes. It was
@@ -878,10 +909,15 @@ created. return t if num is > 0, nil otherwise."
 ; but undo would show the 2 steps, which is bad.
 
 (defun insert-and-expand (s)
-  (let* ((exp (abbrev-expansion s))
-			(c (count-char-in-string empty-hole-string exp)))
+  (let* ((pos (point))
+			(exp (abbrev-expansion s))
+			(c (count-re-in-string empty-hole-regexp exp)))
 	 (insert exp)
-	 (replace-string-by-holes-backward-move-point c empty-hole-string)
+	 (replace-string-by-holes-backward-move-point c empty-hole-regexp)
+	 (if (> c 1) (goto-char pos)
+		(goto-char pos)
+		(set-point-next-hole-destroy) ; if only one hole, go to it.
+		)
 	 )
   )