diff options
-rw-r--r-- | coq/coq-db.el | 19 | ||||
-rw-r--r-- | coq/coq-indent.el | 4 | ||||
-rw-r--r-- | coq/coq-syntax.el | 6 |
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) |