diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2006-08-25 13:21:20 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2006-08-25 13:21:20 +0000 |
| commit | ac2ed5ec6a3fee36abd1ca0aca2f049c1ce0fb01 (patch) | |
| tree | 651d75bca39cbd618bde10ed23483508a522d301 /coq/coq-syntax.el | |
| parent | 079bf430d977dfe5d451ffd1aebff5554801c388 (diff) | |
Adding comments
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 2775ac2d..0c96a79b 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -823,10 +823,21 @@ Used by `coq-goal-command-p'" ;(defconst coq-with-with-hole-regexp ; (concat "\\(" "with" "\\)\\s-+\\(" coq-ids "\\)" "\\(?:[^:]+\\|:[^=]\\)*:=")) +; must match: +; with f := +; with f : foo := +; with f x y := +; with f x y : t := +; with f (x:tx) y := +; with f (x:tx) (y:ty) := +; BUT NOT: +; with f ...(x:=t)... +; the simplest is : +; either no '(' before the first ':' +; OR the first := found follows a ')[^(.]*' +; actually this wont colorize f in 'with f (x:t) : foo.bar :="' but that is acceptable (defconst coq-with-with-hole-regexp - (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(]*:\\|.*)[^(.]*:=\\)") - ;(concat "\\(" "with" "\\)\\s-+\\(" coq-id "\\)" ".*?)[^(.]*:=") - ) + (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(]*:\\|.*)[^(.]*:=\\)")) (defvar coq-font-lock-keywords-1 (append |