diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-08-14 09:05:31 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-08-14 09:05:31 +0000 |
| commit | d6eef2696e6b42d2892f9abf7f867ffbaa110e6d (patch) | |
| tree | 7777b84eeca8dc430c4ef7a9bc64e7c4e3f8966b /isar/isar-syntax.el | |
| parent | db36b5153becb47002d336f93d6972d6b5f9d596 (diff) | |
Do not hide the spurious ASCII characters as it confuses old hands.
Diffstat (limited to 'isar/isar-syntax.el')
| -rw-r--r-- | isar/isar-syntax.el | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index bef302fa..e2590a0d 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -377,15 +377,17 @@ matches contents of quotes for quoted identifiers.") ;; done generically at the moment: ;; (isar-output-flk "\^AM" "\\(?:[^\^A]\\|\^A[^N]\\)*" "\^AN" 'proof-error-face) (isar-output-flk "\^AB" isar-long-id-stuff "\^AA" 'isabelle-class-name-face) - (isar-output-flk "\^AC'" isar-id "\^AA" 'isabelle-tfree-name-face) - (isar-output-flk "\^AD'" isar-idx "\^AA" 'isabelle-tvar-name-face) - (isar-output-flk "\^AD\\?'" isar-idx "\^AA" 'isabelle-tvar-name-face) + (isar-output-flk "\^AC" isar-id "\^AA" 'isabelle-tfree-name-face) + (isar-output-flk "\^AD" isar-idx "\^AA" 'isabelle-tvar-name-face) (isar-output-flk "\^AE" isar-id "\^AA" 'isabelle-free-name-face) (isar-output-flk "\^AF" isar-id "\^AA" 'isabelle-bound-name-face) (isar-output-flk "\^AG" isar-idx "\^AA" 'isabelle-var-name-face) - (isar-output-flk "\^AG\\?" isar-idx "\^AA" 'isabelle-var-name-face) (isar-output-flk "\^AH" isar-id "\^AA" 'proof-declaration-name-face) - (isar-output-flk "\^AH\\?" isar-idx "\^AA" 'proof-declaration-name-face)) + ;; could also hide spurious ASCII characters which + ;; aren't needed when working in colour: + ; (isar-output-flk "\^AG\\?" isar-idx "\^AA" 'isabelle-var-name-face) + ; etc + ) "*Font-lock table for Isabelle output terms.") (defun isar-strip-output-markup (string) |