diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-11 16:55:13 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-11 16:55:13 +0000 |
| commit | b97d82c0af4bf658c28e531b762b87f291f792a5 (patch) | |
| tree | 56fd5698b27c59f9773e8ce1d9c3bcc343bafe87 /isar/isar-syntax.el | |
| parent | 9dd011c360dea5380ec003565c51185644d4c67f (diff) | |
Support custom syntactic fontification.
Diffstat (limited to 'isar/isar-syntax.el')
| -rw-r--r-- | isar/isar-syntax.el | 41 |
1 files changed, 40 insertions, 1 deletions
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) |