First fix of bug introduced by the last font-lock fix. Not finished.

3 files changed, 24 insertions, 5 deletions

diff --git a/coq/coq-db.el b/coq/coq-db.el
index 97e637eb..c8fd3f8a 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -92,13 +92,30 @@ regexp.  See `coq-syntax-db' for DB structure."
   (let ((l db) res)
     (while l
       (let* ((hd (car l)) (tl (cdr l))	; hd is the first infos list
-	     (color (nth 4 hd)))       ; colorization string
+	     (color (concat "\\_<" (nth 4 hd) "\\_>")))       ; colorization string
+;	     (color (nth 4 hd)))       ; colorization string
 	;; TODO delete doublons
 	(when (and color (or (not filter) (funcall filter hd)))
 	  (setq res (nconc res (list color)))) ; careful: nconc destructive!
 	(setq l tl)))
     res))
 
+(defun coq-build-opt-regexp-from-db (db &optional filter)
+  "Take a keyword database DB and return a regexps for font-lock.
+If non-nil Optional argument FILTER is a function applying to each line of DB.
+For each line if FILTER returns nil, then the keyword is not added to the
+regexp.  See `coq-syntax-db' for DB structure."
+  (let ((l db) res)
+    (while l
+      (let* ((hd (car l)) (tl (cdr l))	; hd is the first infos list
+	     (color (nth 4 hd)))       ; colorization string
+	;; TODO delete doublons
+	(when (and color (or (not filter) (funcall filter hd)))
+	  (setq res (nconc res (list color)))) ; careful: nconc destructive!
+	(setq l tl)))
+    (proof-ids-to-regexp res)))
+
+
 ;; Computes the max length of strings in a list
 (defun max-length-db (db)
   "Return the length of the longest first element (menu label) of DB.
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index b0b52e95..6fbb21a3 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -365,8 +365,8 @@ not inside the {} of a record)."
       (goto-char nextpt)
       (cond
        ((proof-looking-at-syntactic-context) ())
-		 ((proof-looking-at-safe proof-indent-close-regexp)
-		  (coq-find-unclosed 1 limit)) ;; recursive call
+       ;; ((proof-looking-at-safe proof-indent-close-regexp)
+       ;;  (coq-find-unclosed 1 limit)) ;; recursive call
        ((proof-looking-at-safe close-re) (setq lvl (+ lvl 1)))
        ((proof-looking-at-safe open-re) (setq lvl (- lvl 1))))
       (setq nextpt (save-excursion (proof-re-search-backward both-re))))
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index e8ec3c12..d6eef807 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -17,7 +17,7 @@
     (dolist (regexp args)
       (setq res (concat res (if (string-equal res "") "\\(?:" "\\|\\(?:")
 			regexp "\\)")))
-    (concat "\\_<\\(?:"res"\\)\\_>")))
+    res))
 
 (eval-when-compile
   (require 'span)
@@ -835,6 +835,8 @@ Used by `coq-goal-command-p'"
 (defvar coq-tactics
   (append coq-state-changing-tactics coq-state-preserving-tactics))
 
+(defvar coq-tactics-regexp (coq-build-opt-regexp-from-db coq-tactics-db))
+
 (defvar coq-retractable-instruct
   (append coq-state-changing-tactics coq-keywords-state-changing-commands))
 
@@ -969,7 +971,7 @@ Group number 1 matches the name of the library which is required.")
     (cons (proof-regexp-alt-list coq-solve-cheat-tactics) 'coq-cheat-face)
     (cons (proof-regexp-alt-list coq-keywords) 'font-lock-keyword-face)
     (cons (proof-regexp-alt-list coq-reserved) 'font-lock-type-face)
-    (cons (proof-regexp-alt-list coq-tactics ) 'proof-tactics-name-face)
+    (cons coq-tactics-regexp 'proof-tactics-name-face)
     (cons (proof-regexp-alt-list coq-tacticals) 'proof-tacticals-name-face)
     (cons (proof-regexp-alt-list (list "Set" "Type" "Prop")) 'font-lock-type-face)
     (cons "============================" 'font-lock-keyword-face)