diff options
| author | Makarius Wenzel | 1999-08-24 16:12:36 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 1999-08-24 16:12:36 +0000 |
| commit | 0f35715b1b71964d36880c7d9e7ea721e41c1bb7 (patch) | |
| tree | 1082f0de2db6e67adadf6d46c02d3eaaf8d48a07 | |
| parent | 61ea68bcc14392f3633bf373d4fb09d473772dff (diff) | |
some output syntax;
| -rw-r--r-- | isar/isar-syntax.el | 32 |
1 files changed, 18 insertions, 14 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 8316828d..52f97ca6 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -55,6 +55,13 @@ (modify-syntax-entry ?\{ "(}1") (modify-syntax-entry ?\} "){4")) +(defun isar-init-output-syntax-table () + "Set appropriate values for syntax table for Isabelle output." + (isar-init-syntax-table) + ;; ignore strings so font-locking works + ;; inside them + (modify-syntax-entry ?\" " ")) + ;; ----- syntax for font-lock and other features @@ -120,7 +127,7 @@ (concat "\\s-*\\(" isar-string "\\|" isar-id "\\)\\s-*") "Regexp matching Isabelle/Isar names, with contents grouped.") -(defvar isar-font-lock-terms +(defvar isar-output-font-lock-terms (list (cons (concat "\351" isar-id "\350") 'proof-declaration-name-face) ; class (cons (concat "\352'" isar-id "\350") 'proof-tacticals-name-face) ; tfree @@ -148,19 +155,16 @@ (defvar isar-font-lock-keywords-1 - (append -;FIXME n.a. -; isar-font-lock-terms - (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-asm) 'proof-declaration-name-face) - (cons (proof-ids-to-regexp isar-keywords-proof-script) 'font-lock-reference-face)))) + (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-asm) 'proof-declaration-name-face) + (cons (proof-ids-to-regexp isar-keywords-proof-script) 'font-lock-reference-face))) ;; ----- variations on undo |