diff options
| author | Makarius Wenzel | 1999-08-18 17:05:22 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 1999-08-18 17:05:22 +0000 |
| commit | 39e2cc196ed9ef9bf7d9f444b47800368872bd0f (patch) | |
| tree | c9902e0d1ce0a58d34a5a72ebe20fb57fefd0886 | |
| parent | c5f898260c420b355a053f5eb753c7f71828bb94 (diff) | |
deactivated isar-font-lock-terms (currently useless);
| -rw-r--r-- | isar/isar-syntax.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index b41a65c8..29342b28 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -149,7 +149,8 @@ (defvar isar-font-lock-keywords-1 (append - isar-font-lock-terms +;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) |