diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2004-04-14 15:53:53 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2004-04-14 15:53:53 +0000 |
| commit | c230e600adeb35f4c174c68812712cf50a45fe44 (patch) | |
| tree | 6d314a91de6187e1d617259e101a6373406b97d0 | |
| parent | b4eafa55c48b39be73947ac67fb8a8dae439c29d (diff) | |
added basic support for imenu for coq.
| -rw-r--r-- | coq/coq-syntax.el | 6 | ||||
| -rw-r--r-- | coq/coq.el | 4 |
2 files changed, 9 insertions, 1 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 122b9e02..6ff24e4d 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -839,6 +839,12 @@ Idtac (Nop) tactic, put the following line in your .emacs: (modify-syntax-entry ?\) ")(4")) +(defconst coq-generic-expression + (mapcar (lambda (kw) + (list (capitalize kw) + (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" ) + 1)) + (append coq-keywords-decl coq-keywords-defn coq-keywords-goal))) (provide 'coq-syntax) @@ -614,7 +614,9 @@ This is specific to coq-mode." proof-really-save-command-p 'coq-save-command-p ;pierre:deals with Proof <term>. proof-save-with-hole-regexp coq-save-with-hole-regexp proof-goal-with-hole-regexp coq-goal-with-hole-regexp - proof-nested-undo-regexp coq-state-changing-commands-regexp) + proof-nested-undo-regexp coq-state-changing-commands-regexp + proof-script-imenu-generic-expression coq-generic-expression + ) (setq ;indentation is implemented in coq-indent.el |