diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-08-14 09:17:33 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-08-14 09:17:33 +0000 |
| commit | 94788d76ea579e48ac9bd5d447de24f3c7f5495e (patch) | |
| tree | 4f3624e69287818963ce2cb7bcecc5f50d0e695a /isar/isar-syntax.el | |
| parent | d6eef2696e6b42d2892f9abf7f867ffbaa110e6d (diff) | |
isar-output-font-lock-keywords-1: enable display of ? and ' again
Diffstat (limited to 'isar/isar-syntax.el')
| -rw-r--r-- | isar/isar-syntax.el | 29 |
1 files changed, 21 insertions, 8 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index e2590a0d..68740351 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -373,18 +373,31 @@ matches contents of quotes for quoted identifiers.") (isar-output-flkprops "\^AW" "\\(?:[^\^A]\\|\^A[^X]\\)*" "\^AX" '(face (:underline t) mouse-face 'highlight sendback t)) - (isar-output-flk "\^A0" "\\(?:[^\^A]\\|\^A[^1]\\)*" "\^A1" 'proof-warning-face) + + (isar-output-flk "\^A0" + "\\(?:[^\^A]\\|\^A[^1]\\)*" "\^A1" + 'proof-warning-face) + ;; 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 "\^AB" isar-long-id-stuff + "\^AA" 'isabelle-class-name-face) + (isar-output-flk "\^AC" (concat "'" isar-id) + "\^AA" 'isabelle-tfree-name-face) + (isar-output-flk "\^AD" (concat "[\\?']?" 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 "\^AH" isar-id "\^AA" 'proof-declaration-name-face) - ;; could also hide spurious ASCII characters which - ;; aren't needed when working in colour: + (isar-output-flk "\^AG" (concat "[\\?]?" isar-idx) + "\^AA" 'isabelle-var-name-face) + (isar-output-flk "\^AH" (concat "[\\?]?" isar-idx) + "\^AA" 'proof-declaration-name-face) + + ;; may alternatively hide the spurious ASCII characters which + ;; aren't needed when working in colour (Isabelle printing switch + ;; allows this for ?'s but not for 's): + ; (isar-output-flk "\^AC'" isar-id "\^AA" 'isabelle-tfree-name-face) ; (isar-output-flk "\^AG\\?" isar-idx "\^AA" 'isabelle-var-name-face) ; etc ) |