diff options
| author | David Aspinall | 1998-11-03 14:41:54 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-11-03 14:41:54 +0000 |
| commit | b8f4c78f6659d6962a810e4b40dda5b34fd0fb47 (patch) | |
| tree | 693218784814055db5625efecb82c9736a605135 | |
| parent | 6d570f591af3d4aa5ded571cea0b70bd83e362fa (diff) | |
More regexp improvements
| -rw-r--r-- | isa/isa-syntax.el | 16 |
1 files changed, 2 insertions, 14 deletions
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el index aac2a556..135a1715 100644 --- a/isa/isa-syntax.el +++ b/isa/isa-syntax.el @@ -140,26 +140,16 @@ :group 'isabelle-config) (defconst isa-string-regexp - (concat "\\s-*\"\\(" isa-id "\"\\)\\s-*") + (concat "\\s-*\"\\(" isa-id "\\)\"\\s-*") "Regexp matching ML strings, with contents bracketed.") (defconst isa-goal-with-hole-regexp (concat "\\(" ;; Don't bother with "val xxx = prove_goal blah". (proof-ids-to-regexp '("qed_goal")) - "\\)" isa-string-regexp ".*;\\s-*$") + "\\)" isa-string-regexp) "Regexp matching goal commands in Isabelle which name a theorem") -;; FIXME: rubbish for Isabelle -(defconst isa-decl-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp isa-keywords-decl) - "\\)\\s-+\\(" isa-ids "\\)\\s-*:")) - -;; FIXME: rubbish for Isabelle -(defconst isa-defn-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp isa-keywords-defn) - "\\)\\s-+\\(" isa-id "\\)\\s-*[:[]")) - (defvar isa-font-lock-keywords-1 (append isa-font-lock-terms @@ -168,8 +158,6 @@ (cons (proof-ids-to-regexp isa-tacticals) 'proof-tacticals-name-face) (list isa-goal-with-hole-regexp 2 'font-lock-function-name-face) - (list isa-decl-with-hole-regexp 2 'proof-declaration-name-face) - (list isa-defn-with-hole-regexp 2 'font-lock-function-name-face) (list isa-save-with-hole-regexp 2 'font-lock-function-name-face)))) (provide 'isa-syntax) |