Support custom syntactic fontification.

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)