diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2000-02-09 10:00:18 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2000-02-09 10:00:18 +0000 |
| commit | 54181a1586d432bb3dafb5a0449420f61e65fbce (patch) | |
| tree | c4a53d59597ff381879ef41abd1e7fec41c57325 /isar/isar-syntax.el | |
| parent | dae4844f4ee11d850ad6be8eef5dffb802189250 (diff) | |
added isar-keywords-qed-global, isar-global-save-command-regexp;
added isar-keywords-indent-reset;
tuned font-lock;
Diffstat (limited to 'isar/isar-syntax.el')
| -rw-r--r-- | isar/isar-syntax.el | 40 |
1 files changed, 28 insertions, 12 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 306b6b13..270ef0ec 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -77,17 +77,18 @@ (defconst isar-keywords-save (append isar-keywords-qed - isar-keywords-qed-block)) + isar-keywords-qed-block + isar-keywords-qed-global)) (defconst isar-keywords-proof-enclose (append isar-keywords-proof-block - isar-keywords-qed isar-keywords-qed-block)) (defconst isar-keywords-proof (append isar-keywords-proof-goal isar-keywords-proof-chain - isar-keywords-proof-decl)) + isar-keywords-proof-decl + isar-keywords-qed)) (defconst isar-keywords-proof-context (append isar-keywords-proof-asm @@ -97,6 +98,10 @@ (append isar-keywords-proof-goal isar-keywords-proof-asm-goal)) +(defconst isar-keywords-proof-improper + (append isar-keywords-proof-script + isar-keywords-qed-global)) + (defconst isar-keywords-outline (append isar-keywords-theory-begin isar-keywords-theory-heading @@ -122,6 +127,14 @@ (append isar-keywords-proof-block isar-keywords-qed-block)) +(defconst isar-keywords-indent-reset + (append isar-keywords-theory-begin + isar-keywords-theory-switch + isar-keywords-theory-end + isar-keywords-theory-heading + isar-keywords-theory-decl + isar-keywords-qed-global)) + ;; ----- regular expressions @@ -140,6 +153,9 @@ (defconst isar-save-command-regexp (proof-anchor-regexp (proof-ids-to-regexp isar-keywords-save))) +(defconst isar-global-save-command-regexp + (proof-anchor-regexp (proof-ids-to-regexp isar-keywords-qed-global))) + (defconst isar-save-with-hole-regexp "$^") ; n.a. (defconst isar-goal-command-regexp @@ -232,15 +248,15 @@ (defvar isar-font-lock-keywords-1 (list - (cons (proof-ids-to-regexp isar-keywords-minor) 'font-lock-type-face) - (cons (proof-ids-to-regexp isar-keywords-control) 'proof-error-face) - (cons (proof-ids-to-regexp isar-keywords-diag) 'proof-tacticals-name-face) - (cons (proof-ids-to-regexp isar-keywords-theory-enclose) 'font-lock-function-name-face) - (cons (proof-ids-to-regexp isar-keywords-theory) 'font-lock-keyword-face) - (cons (proof-ids-to-regexp isar-keywords-proof-enclose) 'font-lock-function-name-face) - (cons (proof-ids-to-regexp isar-keywords-proof) 'font-lock-keyword-face) - (cons (proof-ids-to-regexp isar-keywords-proof-context) 'proof-declaration-name-face) - (cons (proof-ids-to-regexp isar-keywords-proof-script) 'font-lock-reference-face))) + (cons (proof-ids-to-regexp isar-keywords-minor) 'font-lock-type-face) + (cons (proof-ids-to-regexp isar-keywords-control) 'proof-error-face) + (cons (proof-ids-to-regexp isar-keywords-diag) 'proof-tacticals-name-face) + (cons (proof-ids-to-regexp isar-keywords-theory-enclose) 'font-lock-preprocessor-face) + (cons (proof-ids-to-regexp isar-keywords-theory) 'font-lock-keyword-face) + (cons (proof-ids-to-regexp isar-keywords-proof-enclose) 'font-lock-preprocessor-face) + (cons (proof-ids-to-regexp isar-keywords-proof) 'font-lock-keyword-face) + (cons (proof-ids-to-regexp isar-keywords-proof-context) 'proof-declaration-name-face) + (cons (proof-ids-to-regexp isar-keywords-proof-improper) 'font-lock-reference-face))) (defvar isar-output-font-lock-keywords-1 (list |