From 94788d76ea579e48ac9bd5d447de24f3c7f5495e Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 14 Aug 2009 09:17:33 +0000 Subject: isar-output-font-lock-keywords-1: enable display of ? and ' again --- isar/isar-syntax.el | 29 +++++++++++++++++++++-------- 1 file changed, 21 insertions(+), 8 deletions(-) (limited to 'isar/isar-syntax.el') 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 ) -- cgit v1.2.3