diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-10-14 00:50:10 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-10-14 00:50:10 +0000 |
| commit | 9f9ed3af6e012b00f66204003548dc91ec06c7c0 (patch) | |
| tree | 6803c4378c6ecca4c0edbfdc06ddfd0095167fb9 /isar/isar-syntax.el | |
| parent | 0b518a557ac527837494e97cf7a315e123d16d3b (diff) | |
Remove fume settings
Diffstat (limited to 'isar/isar-syntax.el')
| -rw-r--r-- | isar/isar-syntax.el | 37 |
1 files changed, 8 insertions, 29 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 8724e80d..a014337b 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -138,13 +138,6 @@ This list is in the right format for proof-easy-config.") (defconst isar-keywords-outline (mapcar 'car isar-keyword-level-alist)) -(defconst isar-keywords-fume - (append isar-keywords-theory-begin - isar-keywords-theory-heading - isar-keywords-theory-decl - isar-keywords-theory-script - isar-keywords-theory-goal)) - (defconst isar-keywords-indent-open (append isar-keywords-theory-goal isar-keywords-proof-goal @@ -500,28 +493,14 @@ matches contents of quotes for quoted identifiers.") isar-name-regexp)) -;; ----- function-menu and imenu - -(defconst isar-any-entity-regexp - (concat "\\(?:" (isar-ids-to-regexp isar-keywords-fume) "\\)" - "\\(?:\\s-*(\\s-*in[^)]+)\\)?" - "\\(?:" isar-name-regexp "[[:=]\\)")) +;; ----- imenu -(defconst isar-named-entity-regexp - (concat "\\(" (isar-ids-to-regexp isar-keywords-fume) "\\)" - "\\(?:\\s-*(\\s-*in[^)]+)\\)?" - isar-name-regexp "[[:=]" )) - -(defconst isar-unnamed-entity-regexp - (concat "\\(" (isar-ids-to-regexp isar-keywords-fume) "\\)")) - -(defconst isar-next-entity-regexps - (list isar-any-entity-regexp - (list isar-named-entity-regexp '(1 3)))) -;; da: I've removed unnamed entities, they clutter the menu -;; NB: to add back, need ? at end of isar-any-entity-regexp -;; (list isar-unnamed-entity-regexp 1))) -;; Might also remove heading +(defconst isar-keywords-imenu + (append isar-keywords-theory-begin + isar-keywords-theory-heading + isar-keywords-theory-decl + isar-keywords-theory-script + isar-keywords-theory-goal)) (defconst isar-generic-expression (mapcar (lambda (kw) @@ -530,7 +509,7 @@ matches contents of quotes for quoted identifiers.") "\\(?:\\s-*(\\s-*in[^)]+)\\)?" isar-name-regexp "[[:=]") 1)) - isar-keywords-fume)) + isar-keywords-imenu)) ;; ----- indentation |