diff options
| -rw-r--r-- | isa/x-symbol-isabelle.el | 4 | ||||
| -rw-r--r-- | isar/isar-syntax.el | 10 | ||||
| -rw-r--r-- | isar/isar.el | 22 |
3 files changed, 22 insertions, 14 deletions
diff --git a/isa/x-symbol-isabelle.el b/isa/x-symbol-isabelle.el index a5fe0126..eb6facb7 100644 --- a/isa/x-symbol-isabelle.el +++ b/isa/x-symbol-isabelle.el @@ -113,9 +113,7 @@ or subscript tag." ;; the [\350-\357].\350\\|\^A[A-H].\^AA part is there to enable single ;; char sub/super scripts with coloured Isabelle output. (defcustom x-symbol-isabelle-single-char-regexp - (if (eq proof-assistant-symbol 'isar) - "\^A[A-H].\^AA\\|[^\\]\\|\\\\<[A-Za-z0-9_']+>" - "[\350-\357].\350\\|\^A[A-H].\^AA\\|[^\\]\\|\\\\\\\\?<[A-Za-z0-9_']+>") + "[\350-\357].\350\\|\^A[A-H].\^AA\\|[^\\]\\|\\\\\\\\?<[A-Za-z0-9_']+>" "Return regexp matching \<ident> or c for some char c." :group 'x-symbol-isabelle :type 'regexp) diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 0f0379ec..f9f7bd1b 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -358,6 +358,16 @@ matches contents of quotes for quoted identifiers.") (defvar isar-output-font-lock-keywords-1 (list + (cons (concat "\351" isar-long-id-stuff "\350") 'isabelle-class-name-face) + (cons (concat "\352'" isar-id "\350") 'isabelle-tfree-name-face) + (cons (concat "\353'" isar-idx "\350") 'isabelle-tvar-name-face) + (cons (concat "\353\\?'" isar-idx "\350") 'isabelle-tvar-name-face) + (cons (concat "\354" isar-id "\350") 'isabelle-free-name-face) + (cons (concat "\355" isar-id "\350") 'isabelle-bound-name-face) + (cons (concat "\356" isar-idx "\350") 'isabelle-var-name-face) + (cons (concat "\356\\?" isar-idx "\350") 'isabelle-var-name-face) + (cons (concat "\357" isar-id "\350") 'proof-declaration-name-face) + (cons (concat "\357\\?" isar-idx "\350") 'proof-declaration-name-face) (cons (concat "\^AB" isar-long-id-stuff "\^AA") 'isabelle-class-name-face) (cons (concat "\^AC'" isar-id "\^AA") 'isabelle-tfree-name-face) (cons (concat "\^AD'" isar-idx "\^AA") 'isabelle-tvar-name-face) diff --git a/isar/isar.el b/isar/isar.el index d4fe03cd..1d1fe5c4 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -182,8 +182,8 @@ See -k option for Isabelle interface script." (defun isar-shell-mode-config-set-variables () "Configure generic proof shell mode variables for Isabelle/Isar." (setq - proof-shell-wakeup-char ?\^A - proof-shell-annotated-prompt-regexp "^\\w*[>#] \^AS" + proof-shell-wakeup-char nil + proof-shell-annotated-prompt-regexp "^\\w*[>#] \372\\|^\\w*[>#] \^AS" ;; This pattern is just for comint. proof-shell-prompt-pattern "^\\w*[>#] " @@ -205,8 +205,8 @@ See -k option for Isabelle interface script." '(("\\\\" . "\\\\") ("\"" . "\\\""))) proof-shell-proof-completed-regexp nil ; n.a. - proof-shell-interrupt-regexp "\^AM\\*\\*\\* Interrupt" - proof-shell-error-regexp "\^AM\\*\\*\\*" + proof-shell-interrupt-regexp "\364\\*\\*\\* Interrupt\\|\^AM\\*\\*\\* Interrupt" + proof-shell-error-regexp "\364\\*\\*\\*\\|\^AM\\*\\*\\*" proof-shell-abort-goal-regexp nil ; n.a. ;; @@ -216,8 +216,8 @@ See -k option for Isabelle interface script." ;; matches names of assumptions proof-shell-assumption-regexp isar-id - proof-shell-start-goals-regexp "\^AO\n" - proof-shell-end-goals-regexp "\^AP" + proof-shell-start-goals-regexp "\366\n\\|\^AO\n" + proof-shell-end-goals-regexp "\367\\|\^AP" ;; FIXME: next one is needed for backward compatibility. ;; Would be nice to remove this somehow else, it's only used for @@ -230,8 +230,8 @@ See -k option for Isabelle interface script." proof-shell-restart-cmd "ProofGeneral.restart" proof-shell-eager-annotation-start-length 1 - proof-shell-eager-annotation-start "\^AI\\|\^AK" - proof-shell-eager-annotation-end "\^AJ\\|\^AL" + proof-shell-eager-annotation-start "\360\\|\362\\|\^AI\\|\^AK" + proof-shell-eager-annotation-end "\361\\|\363\\|\^AJ\\|\^AL" ;; see isar-pre-shell-start for proof-shell-trace-output-regexp ;; Isabelle is learning to talk PGIP... @@ -244,7 +244,7 @@ See -k option for Isabelle interface script." proof-shell-clear-goals-regexp "Proof General, please clear the goals buffer." ;; Theorem dependencies. NB: next regex anchored at end with eager annot end - proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies of \\(.*\\) are \"\\(.*\\)\"\\(\^AJ\\)" + proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies of \\(.*\\) are \"\\(.*\\)\"\\(\361\\|\^AJ\\)" proof-shell-theorem-dependency-list-split "\" \"" proof-shell-show-dependency-cmd "thm %s;" proof-shell-identifier-under-mouse-cmd @@ -255,7 +255,7 @@ See -k option for Isabelle interface script." ;; Allow font-locking for output based on hidden annotations, see ;; isar-output-font-lock-keywords-1 pg-use-specials-for-fontify t - pg-special-char-regexp "\^A[A-Z]" + pg-special-char-regexp "[\200-\377]\\|\^A[A-Z]" pg-after-fontify-output-hook 'pg-remove-specials pg-subterm-help-cmd "term %s" @@ -563,7 +563,7 @@ Checks the width in the `proof-goals-buffer'" (setq proof-mode-for-shell 'isar-shell-mode) (setq proof-mode-for-goals 'isar-goals-mode) (setq proof-mode-for-response 'isar-response-mode) - (setq proof-shell-trace-output-regexp "\^AV")) + (setq proof-shell-trace-output-regexp "\375\\|\^AV")) ;; |