diff options
Diffstat (limited to 'isar')
-rw-r--r-- | isar/isabelle-system.el | 1 | ||||
-rw-r--r-- | isar/isar-autotest.el | 8 | ||||
-rw-r--r-- | isar/isar-syntax.el | 41 | ||||
-rw-r--r-- | isar/isar.el | 6 |
4 files changed, 47 insertions, 9 deletions
diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el index df4abb59..fa7fe72c 100644 --- a/isar/isabelle-system.el +++ b/isar/isabelle-system.el @@ -19,6 +19,7 @@ (require 'scomint) (require 'proof-site) (require 'proof-menu) + (require 'proof-syntax) (proof-ready-for-assistant 'isar) ; compile for isar (defvar proof-assistant-menu nil)) diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index bee8d15a..19fe473a 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -32,6 +32,10 @@ (pg-autotest eval (isar-tracing:auto-solve-toggle 0)) ; autosolve hammers this! (pg-autotest eval (proof-full-annotation-toggle 0)) (pg-autotest script-wholefile "etc/isar/AHundredTheorems.thy") + + (pg-autotest remark "Now in tokens mode") + (pg-autotest eval (proof-unicode-tokens-toggle)) + (pg-autotest script-wholefile "isar/Example-Tokens.thy") (pg-autotest script-wholefile "isar/ex/Tarski.thy") (pg-autotest remark "Testing random jumps") @@ -41,10 +45,6 @@ (pg-autotest remark "Testing restarting the prover") (pg-autotest quit-prover) - (pg-autotest remark "Now in tokens mode") - (pg-autotest eval (proof-unicode-tokens-toggle)) - (pg-autotest script-wholefile "isar/Example-Tokens.thy") - (pg-autotest remark "Simple test of multiple file behaviour:") (pg-autotest script-wholefile "etc/isar/multiple/C.thy") diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 6b48cce7..d1d2c1f1 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -288,7 +288,7 @@ matches contents of quotes for quoted identifiers.") (:foreground "springgreen4") (:background "springgreen1") (:italic t)) - "*Face used instead of `font-lock-string-face' for Isar." + "*Face for fontifying string contents in Isabelle." :group 'proof-faces) (defface isabelle-class-name-face @@ -339,6 +339,7 @@ matches contents of quotes for quoted identifiers.") "*Face for Isabelle term / type highlighting" :group 'proof-faces) +(defconst isabelle-string-face 'isabelle-string-face) (defconst isabelle-class-name-face 'isabelle-class-name-face) (defconst isabelle-tfree-name-face 'isabelle-tfree-name-face) (defconst isabelle-tvar-name-face 'isabelle-tvar-name-face) @@ -347,6 +348,44 @@ matches contents of quotes for quoted identifiers.") (defconst isabelle-var-name-face 'isabelle-var-name-face) +;; font-lock syntactic fontification + +;; adapted from font-lock.el in GNU Emacs 23.1.1 +(defun isar-font-lock-fontify-syntactically-region + (start end &optional loudly ppss) + "Put proper face on each string and comment between START and END. +START should be at the beginning of a line." + (let ((comment-end-regexp + (replace-regexp-in-string "^ *" "" comment-end)) + state beg) + (if loudly (message "Fontifying %s... (syntactically...)" (buffer-name))) + (goto-char start) + ;; + ;; Find the `start' state. + (setq state (or ppss (syntax-ppss start))) + ;; + ;; Find each interesting place between here and `end'. + (while + (let ((instring (nth 3 state)) + (incomment (nth 4 state))) + (when (or instring incomment) + (setq beg (max (nth 8 state) start)) + (setq state (parse-partial-sexp (point) end nil nil state + 'syntax-table)) + (cond + (instring + (put-text-property (1+ beg) + (1- (point)) 'face isabelle-string-face) + (put-text-property beg (1+ beg) 'face proof-boring-face) + (put-text-property (1- (point)) (point) 'face proof-boring-face)) + (t + (put-text-property beg (point) 'face font-lock-comment-face)))) + (< (point) end)) + (setq state (parse-partial-sexp (point) end nil nil state + 'syntax-table))))) + +;; font-lock keywords fontification + (defvar isar-font-lock-keywords-1 (list (cons 'isar-match-nesting 'font-lock-preprocessor-face) diff --git a/isar/isar.el b/isar/isar.el index dad9f871..92ef0b9d 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -1,6 +1,6 @@ ;; isar.el --- Major mode for Isabelle/Isar proof assistant ;; -;; Copyright (C) 1994-2009 LFCS Edinburgh. +;; Copyright (C) 1994-2010 LFCS Edinburgh. ;; ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; @@ -126,7 +126,7 @@ See -k option for Isabelle interface script." proof-indent-open-regexp isar-indent-open-regexp proof-indent-close-regexp isar-indent-close-regexp - ;; proof engine commands + ;; proof engine proof-showproof-command "pr" proof-goal-command "lemma \"%s\"" proof-save-command "qed" @@ -606,8 +606,6 @@ Uses variables `string' and `scriptspan' passed by dynamic scoping." (isar-mode-config-set-variables) (isar-init-syntax-table) (setq proof-script-font-lock-keywords isar-font-lock-keywords-1) - (set (make-local-variable 'font-lock-string-face) - 'isabelle-string-face) (set (make-local-variable 'comment-quote-nested) nil) ;; can cope with nested comments (set (make-local-variable 'outline-regexp) isar-outline-regexp) (set (make-local-variable 'outline-heading-end-regexp) |