Started the coq-insert-tactic.

2 files changed, 33 insertions, 22 deletions

diff --git a/lib/holes.el b/lib/holes.el
index 3b182f19..529637bd 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -820,33 +820,44 @@ created.  Return the number of holes created."
 	  "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)
+  "Put holes between POS and point, backward, indenting.
+\"#\" and \"@{..}\" between this positions will become holes."
+  (save-excursion (indent-region pos (point) nil))
+  (let ((n (holes-replace-string-by-holes-backward pos)))
+    (case n
+      (0 nil)				; no hole, stay here.
+      (1
+       (goto-char pos)
+       (holes-set-point-next-hole-destroy)) ; if only one hole, go to it.
+      (t
+       (goto-char pos)
+       (message (substitute-command-keys
+		 "\\[holes-set-point-next-hole-destroy] to jump to active hole.  \\[holes-short-doc] to see holes doc."))))))
+
+
+
 (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."
-  (let ((pos last-abbrev-location))
-    (save-excursion (indent-region pos (point) nil))
-    (let ((n (holes-replace-string-by-holes-backward pos)))
-      (case n
-	(0 nil)				; no hole, stay here.
-	(1
-	 (goto-char pos)
-	 (holes-set-point-next-hole-destroy)) ; if only one hole, go to it.
-	(t
-	 (goto-char pos)
-	 (message (substitute-command-keys
-		   "\\[holes-set-point-next-hole-destroy] to jump to active hole.  \\[holes-short-doc] to see holes doc.")))))))
+  (holes-replace-string-by-holes-backward-jump last-abbrev-location))
+
+
 
 (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)))
-    (insert (abbrev-expansion s))
-    (let ((last-abbrev-location pos))
-      (holes-abbrev-complete))))
+  (let ((pos (point))
+	(ins (abbrev-expansion s)))
+    (insert (or ins s))
+    (setq last-abbrev-location pos)
+    (holes-abbrev-complete)))
 
 (defvar holes-mode nil
   "Is equal to t if holes mode is on, nil otherwise.")
diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el
index 7038ebf9..a79a870f 100644
--- a/lib/local-vars-list.el
+++ b/lib/local-vars-list.el
@@ -118,15 +118,10 @@ variable definition (or at the \"End:\" line)."
       (search-forward lpat eol)
       (re-search-forward "\\([^ :]+\\):" eol)
       (let ((varname (match-string 1)))
-	(message "varname = %s" varname)
 	(cond 
 	 ((string-equal varname "End") (setq endreached t) (beginning-of-line))
 	 ((string-equal varname symbname) (setq found t))
-	 (t (forward-line 1) (beginning-of-line))
-	 ))
-      (message "found %s" found)
-      (message "endreached %s" endreached)
-      )
+	 (t (forward-line 1) (beginning-of-line)))))
     (if found t nil)))
 
 
@@ -192,6 +187,11 @@ Raises an error if symb is not in the list."
       (beginning-of-line)
       (local-vars-list-get-current lpat rpat))))
 
+(defun local-vars-list-get-safe (symb)
+  "Return true if variable SYMB belongs to the local variable list of the current
+buffer."
+  (condition-case nil (local-vars-list-get symb) (error nil)))
+
 (defun local-vars-list-set (symb val)
   "Write the value val in the local variable list for variable symb.
 If the variable is already specified in the list, replace the value. If no local