Next round of fixups for font-lock and x-symbol.

8 files changed, 184 insertions, 79 deletions

diff --git a/etc/junk.el b/etc/junk.el
index 46da7f0c..d16b7f61 100644
--- a/etc/junk.el
+++ b/etc/junk.el
@@ -57,3 +57,13 @@ arrive."
 ;      (setq font-lock-defaults '(proof-font-lock-defaults)))))
       ; (put major-mode 'font-lock-defaults (list flks)))))
 
+
+
+;; dump str to buffer ug for testing.
+(defun ugit (str)
+  (save-excursion
+    (set-buffer (get-buffer-create "ug"))
+    (goto-char (point-max))
+    (insert str)
+    (newline)
+    (newline)))
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 7703c08e..4ec803ee 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -121,6 +121,10 @@ inside your Emacs."
   :set 'proof-set-bool
   :group 'proof-user-options)
 
+(defcustom proof-output-fontify-enable t
+  "*Whether to fontify output from the proof assistant."
+  :type 'boolean
+  :group 'proof-user-options)
 
 (defcustom proof-strict-read-only 
   ;; For FSF Emacs, strict read only is buggy when used in
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 5805d0e6..535cf0a8 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2282,20 +2282,8 @@ finish setup which depends on specific proof assistant configuration."
 
   ;;
   ;; Fontlock.
-  ;; 
-  ;; At the moment, the specific code hacks font-lock-keywords.
-  ;; Here we use the value there to hack font-lock-defaults, which
-  ;; is used by font-lock to set font-lock-keywords from again!!  
-  ;; Yuk.
-  ;; Previously, font-lock-keywords was used directly as a setting
-  ;; for the defaults.  This has a bad interaction with x-symbol
-  ;; which edits font-lock-keywords and loses the setting.  
-  ;; So we make a copy of it in a new variable.
-  ;; 
-  (make-local-variable 'font-lock-defaults) ; not needed in XEmacs, FSF?
-  (make-local-variable 'proof-font-lock-defaults)
-  (setq proof-font-lock-defaults font-lock-keywords)
-  (setq font-lock-defaults '(proof-font-lock-defaults))
+  ;;
+  (proof-font-lock-configure-defaults)
 
   ;; FIXME (da): zap commas support is too specific, should be enabled
   ;; by each proof assistant as it likes.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f6a23800..2b948fa2 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -687,8 +687,8 @@ This is a list of tuples of the form (TYPE . STRING). type is either
 	  (insert string)
 	(insert (substring out 0 op)))
       
-      ;; Display special characters
-      (proof-x-symbol-decode-region (point-min) (point-max))
+      ;; Get fonts and characters right
+      (proof-fontify-region (point-min) (point-max))
 
       (proof-display-and-keep-buffer proof-goals-buffer (point-min))
 
@@ -760,6 +760,24 @@ This is a list of tuples of the form (TYPE . STRING). type is either
       (incf ip))
     (substring out 0 op)))
 
+(defun proof-shell-strip-eager-annotation-specials (string)
+  "Strip special eager annotations from STRING, returning cleaned up string.
+The input STRING should be annotated with expressions matching
+proof-shell-eager-annotation-start and eager-annotation-end.
+We only strip specials from the annotations."
+  (let* ((mstart (progn
+		   (string-match proof-shell-eager-annotation-start string)
+		   (match-end 0)))
+	 (mend	 (string-match proof-shell-eager-annotation-end string))
+	 (msg	 (substring string mstart mend))
+	 (strtan (substring string 0 mstart))
+	 (endan	 (substring string mend)))
+    (concat
+     (proof-shell-strip-special-annotations strtan)
+     msg
+     (proof-shell-strip-special-annotations endan))))
+     
+
 (defun proof-shell-handle-output (start-regexp end-regexp append-face)
   "Displays output from `proof-shell-buffer' in `proof-response-buffer'.
 The region in `proof-shell-buffer begins with the first match 
@@ -780,7 +798,7 @@ Returns the string (with faces) in the specified region."
       (setq string
 	    (if proof-shell-leave-annotations-in-output
 		(buffer-substring start end)
-	      (proof-shell-strip-special-annotations 
+	      (proof-shell-strip-special-annotations
 	       (buffer-substring start end)))))
     ;; Erase if need be, and erase next time round too.
     (proof-shell-maybe-erase-response t nil)
@@ -822,7 +840,7 @@ See the documentation for `proof-shell-delayed-output' for further details."
 	(proof-shell-maybe-erase-response t nil)
 	(setq pos (point))
 	(insert str)
-	  (proof-x-symbol-decode-region pos (point))
+	(proof-fontify-region pos (point))
 	(proof-display-and-keep-buffer proof-response-buffer)))
      ;;
      ;; 2. Text to be inserted in goals buffer
@@ -874,7 +892,7 @@ Then we call `proof-shell-handle-error-hook'. "
 	(set-buffer proof-goals-buffer)
 	(erase-buffer)
 	(insert (cdr proof-shell-delayed-output))
-        (proof-x-symbol-decode-region (point-min) (point-max))
+        (proof-fontify-region (point-min) (point-max))
 	(proof-display-and-keep-buffer proof-goals-buffer)))
 
   ;; This prevents problems if the user types in the
@@ -1220,13 +1238,9 @@ Assume proof-script-buffer is active."
 (defun proof-shell-process-urgent-message (message)
   "Analyse urgent MESSAGE for various cases.
 Cases are: included file, retracted file, cleared response buffer, or
-if none of these apply, display it."
-  (save-excursion
-    (set-buffer (get-buffer-create "ug"))
-    (goto-char (point-max))
-    (insert "Hello!")
-    (insert message)
-    (newline))
+if none of these apply, display it.
+MESSAGE should be a string annotated with 
+proof-shell-eager-annotation-start, proof-shell-eager-annotation-end."
     (cond
    ;; Is the prover processing a file?
    ;; FIXME da: this interface is quite restrictive: might be
@@ -1329,9 +1343,14 @@ if none of these apply, display it."
     ;; Don't bother remove the window for the response buffer
     ;; because we're about to put a message in it.
     (proof-shell-maybe-erase-response nil nil)
-    (proof-shell-message message)
-    (proof-response-buffer-display message
-				   'proof-eager-annotation-face))))
+    (let ((stripped	(proof-shell-strip-special-annotations message)))
+      (if (< 100 (length stripped))	;; approx test for multi-line msg
+	  (proof-shell-message stripped))
+      (proof-response-buffer-display 
+       (if proof-shell-leave-annotations-in-output
+	   message
+	 stripped)
+       'proof-eager-annotation-face)))))
 
 (defvar proof-shell-urgent-message-marker nil
   "Marker in proof shell buffer pointing to end of last urgent message.")
@@ -1360,8 +1379,7 @@ This is a subroutine of proof-shell-filter."
 	  (save-excursion
 	    (setq lastend end)
 	    (proof-shell-process-urgent-message
-	     (proof-shell-strip-special-annotations 
-	      (buffer-substring start end))))))
+	     (buffer-substring start end)))))
     ;; Set the marker to the (character after) the end of the last
     ;; message found, if any.  Must take care to keep the marker
     ;; behind the process marker otherwise no output is seen!
@@ -1510,7 +1528,7 @@ however, are always processed; hence their name)."
 		      ;;  expensive; but perhaps we could cut and paste
 		      ;;  from here to the goals buffer to
 		      ;;  avoid duplicating effort?
-		      ;; (proof-x-symbol-decode-region startpos (point))
+		      ;; (proof-fontify-region startpos (point))
 		      (setq string (buffer-substring startpos (point)))
 		      (goto-char (point-max))	
 		      (proof-shell-filter-process-output string)))))))))
@@ -1688,40 +1706,19 @@ before and after sending the command."
 		  (cons proof-general-name proof-shell-menu))
 
 
-
-(defun proof-font-lock-configure-defaults ()
-  "Set defaults for font-lock based on current font-lock-keywords."
-  ;; setting font-lock-defaults explicitly is required by FSF Emacs
-  ;; 20.2's version of font-lock
-  (make-local-variable 'font-lock-defaults) ; not needed in XEmacs, FSF?
-  (make-local-variable 'proof-font-lock-defaults)
-  (setq proof-font-lock-defaults font-lock-keywords)
-  (setq font-lock-defaults '(proof-font-lock-defaults))
-  ;; Turn on fontification only if the user has configured it
-  ;; everywhere in general.
-  (if font-lock-auto-fontify
-      (turn-on-font-lock)))
-
 (defun proof-goals-config-done ()
   "Initialise the goals buffer after the child has been configured."
   (save-excursion
     (set-buffer proof-goals-buffer)
     (proof-font-lock-configure-defaults)
-    ;; Turn off the display of annotations here
-    (proof-shell-dont-show-annotations)
-    ;; Maybe turn on x-symbols
-    (proof-x-symbol-mode)))
+    (proof-x-symbol-configure)))
 
 (defun proof-response-config-done ()
   "Initialise the response buffer after the child has been configured."
   (save-excursion
     (set-buffer proof-response-buffer)
     (proof-font-lock-configure-defaults)
-    ;; Turn off the display of annotations here
-    (proof-shell-dont-show-annotations)
-    ;; Maybe turn on x-symbols
-    (proof-x-symbol-mode)))
-
+    (proof-x-symbol-configure)))
 
 (defun proof-shell-config-done ()
   "Initialise the specific prover after the child has been configured.
@@ -1745,9 +1742,9 @@ processing."
       ;; Send intitialization command and wait for it to be
       ;; processed.   Also ensure that proof-action-list is
       ;; initialised. 
+      (setq proof-action-list nil)
       (if proof-shell-init-cmd
-	  (proof-shell-invisible-command proof-shell-init-cmd t)
-	(setq proof-action-list nil))
+	  (proof-shell-invisible-command proof-shell-init-cmd t))
       
       ;; Configure for x-symbol
       (proof-x-symbol-shell-config))))
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 37819d8b..f5c7668b 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -96,6 +96,9 @@ Default is comma separated, or SEPREGEXP if set."
 
 ;;FIXME: Under FSF Emacs 20.2, when initially fontifying the buffer,
 ;;       commas are not zapped. 
+;; 
+;; FIXME da: this should be more specific!!
+;;
 (defun proof-zap-commas-region (start end &optional length)
   "Remove the face of all `,' within the region (START,END).
 The optional argument LENGTH has no effect. It is required so that we
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index 697956e3..0d15d18e 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -66,9 +66,10 @@ The package is available at http://www.fmi.uni-passau.de/~wedler/x-symbol"))
        ((not (condition-case ()
 		 (require xs-feature-sym) ;; NB: lose all errors!
 	       (t (featurep xs-feature-sym))))
- (format
-  "Proof General: for x-symbol support, you must provide a library %s.el"
-  xs-feature))
+	(funcall error-or-warn 
+		 (format
+ "Proof General: for x-symbol support, you must provide a library %s.el"
+		  xs-feature)))
        (t
 	;;
 	;; We've got everything we need!   So initialize.
@@ -124,8 +125,7 @@ The package is available at http://www.fmi.uni-passau.de/~wedler/x-symbol"))
 ;;;###autoload
 (defun proof-x-symbol-enable ()
   "Turn on or off support for x-symbol, initializing if necessary."
-  (if ;(and proof-x-symbol-enable (not proof-x-symbol-initialized))
-      proof-x-symbol-enable
+  (if (and proof-x-symbol-enable (not proof-x-symbol-initialized))
       (progn
 	(setq proof-x-symbol-enable nil) ; assume failure!
 	(proof-x-symbol-initialize 'giveerrors)
@@ -138,8 +138,9 @@ The package is available at http://www.fmi.uni-passau.de/~wedler/x-symbol"))
       (proof-customize-toggle proof-x-symbol-enable))
 
 (defun proof-x-symbol-decode-region (start end) 
-  "Call (x-symbol-decode-region START END), if x-symbol support is enabled."
-  (if proof-x-symbol-enable
+  "Call (x-symbol-decode-region A Z), if x-symbol support is enabled.
+This converts tokens in the region into X-Symbol characters."
+  (if (and proof-x-symbol-enable)
       (x-symbol-decode-region start end)))
 
 (defun proof-x-symbol-encode-shell-input ()
@@ -166,6 +167,8 @@ A value for proof-shell-insert-hook."
   (save-excursion			; needed or point moves: why?
     (if proof-x-symbol-initialized
 	(progn
+	  ;; Buffers which have XS minor mode toggled always keep 
+	  ;; x-symbol-language set.
 	  (setq x-symbol-language proof-assistant-symbol)
 	  (if (eq x-symbol-mode (not proof-x-symbol-enable))
 	      ;; toggle x-symbol-mode
@@ -180,23 +183,39 @@ A value for proof-shell-insert-hook."
 		;; contents) have changed. I think x-symbol
 		;; ought to do this really!
 		(font-lock-fontify-buffer)))))))
-	  
+
+(defun proof-x-symbol-configure ()
+  "Configure the current buffer for X-Symbol."
+  (if proof-x-symbol-enable
+      (setq x-symbol-language proof-assistant-symbol)
+    (setq x-symbol-language nil)))
+
 (defun proof-x-symbol-mode-all-buffers ()
-  "Activate/deactivate x-symbol mode in all Proof General buffers.
+  "Activate/deactivate x-symbols in all Proof General buffers.
 A subroutine of proof-x-symbol-enable."
+  ;; Shell has its own routine
   (proof-with-current-buffer-if-exists 
    proof-shell-buffer
    (proof-x-symbol-shell-config))
+  ;; Response and goals buffer are fontified/decoded 
+  ;; manually in the code.
+  (proof-with-current-buffer-if-exists 
+   proof-goals-buffer
+   (proof-x-symbol-configure)
+   (proof-fontify-buffer))
+  (proof-with-current-buffer-if-exists 
+   proof-response-buffer
+   (proof-x-symbol-configure)
+   (proof-fontify-buffer))
+  ;; Script buffers are in x-symbol mode
   (let
-      ((bufs   (append
-		(list proof-goals-buffer proof-response-buffer)
-		(proof-buffers-in-mode proof-mode-for-script))))
+      ((bufs (proof-buffers-in-mode proof-mode-for-script)))
     (while bufs
       ;; mapcar doesn't work with macros
-      (proof-with-current-buffer-if-exists (car bufs)
-					   (proof-x-symbol-mode))
+      (with-current-buffer (car bufs) (proof-x-symbol-mode))
       (setq bufs (cdr bufs)))))
 
+
 ;; #### autoload
 (defun proof-x-symbol-shell-config ()
   "Configure the proof shell for x-symbol, if proof-x-symbol-support<>nil.
diff --git a/generic/proof.el b/generic/proof.el
index 95e70c07..a1bc4586 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -82,6 +82,9 @@
 (autoload 'proof-x-symbol-mode "proof-x-symbol"
   "Turn on or off x-symbol mode in the current buffer.")
 
+(autoload 'proof-x-symbol-configure "proof-x-symbol"
+  "Configure the current buffer for X-Symbol.")
+
 ;;;
 ;;; Global variables
 ;;;
@@ -141,7 +144,6 @@ read.")
   "End-of-line string for proof process.")
 
 
-
 ;;;
 ;;; Utilities/macros used in several files  (-> proof-utils)
 ;;;
@@ -220,13 +222,91 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
    kbl))
 
 ;; -----------------------------------------------------------------
+;; Managing font-lock
+;;
+
+;; Buffers which are output only are *not* kept in special minor
+;; modes font-lock-mode (or x-symbol-mode).  In case the user
+;; doesn't want fontification we have a user option,
+;; proof-fontify-output.
+
+(deflocal proof-font-lock-defaults nil
+  "Default value for font-lock-keywords in this buffer.
+We set font-lock-defaults to '(proof-font-lock-defaults) for
+compatibility with X-Symbol, which may hack proof-font-lock-defaults
+with extra patterns (in non-mule mode).")
+
+(defun proof-font-lock-configure-defaults ()
+  "Set defaults for font-lock based on current font-lock-keywords."
+  ;;
+  ;; At the moment, the specific assistant code hacks
+  ;; font-lock-keywords.  Here we use that value to hack
+  ;; font-lock-defaults, which is used by font-lock to set
+  ;; font-lock-keywords from again!!  Yuk.
+  ;;
+  ;; Previously, 'font-lock-keywords was used directly as a setting
+  ;; for the defaults.  This has a bad interaction with x-symbol which
+  ;; edits font-lock-keywords and loses the setting.  So we make a
+  ;; copy of it in a new local variable, proof-font-lock-defaults.
+  ;;
+  (make-local-variable 'font-lock-defaults) ; not needed in XEmacs, FSF?
+  (setq proof-font-lock-defaults font-lock-keywords)
+  ;; Setting font-lock-defaults explicitly is required by FSF Emacs
+  ;; 20.2's version of font-lock in any case.
+  (setq font-lock-defaults '(proof-font-lock-defaults)))
+
+
+(defun proof-fontify-region (start end)
+  "Fontify and decode X-Symbols in region START...END.
+Fontifies according to the buffer's font lock defaults.
+Uses proof-x-symbol-decode to decode tokens if x-symbol is present.
+
+If proof-shell-leave-annotations-in-output is set, remove characters
+with top bit set after fontifying so they can be used for
+fontification.
+
+Returns new END value."
+  ;; We fontify first because decoding changes char positions.
+  ;; It's okay because x-symbol-decode works even without font lock.
+  ;; Possible disadvantage is that font lock patterns can't refer
+  ;; to X-Symbol characters.  Probably they shouldn't!
+  (narrow-to-region start end)
+  (if proof-output-fontify-enable
+      (let ((font-lock-keywords proof-font-lock-defaults))
+	(font-lock-fontify-region start end)
+	;; FIXME: this should be optional, really.
+	(proof-zap-commas-region start end)))
+  (if proof-shell-leave-annotations-in-output
+      ;; Remove special characters that were used for font lock,
+      ;; so cut and paste works from here.
+      (let ((p (point)))
+	(goto-char start)
+	(while (< (point) (point-max))
+	  (forward-char)
+	  (unless (< (char-to-int (char-before (point))) 128)
+	    (delete-char -1)))
+	(goto-char p)))
+  (proof-x-symbol-decode-region start (point-max))
+  (prog1 (point-max)
+    (widen)))
+
+;; FIXME todo: add toggle for fontify region which turns it on/off
+;; (maybe).
+
+(defun proof-fontify-buffer ()
+  "Call proof-fontify-region on whole buffer."
+  (proof-fontify-region (point-min) (point-max)))
+
+
+
+;; -----------------------------------------------------------------
 ;; Display functions
+;;
+
 
-;; FIXME: this function should be combined with
-;; proof-shell-maybe-erase-response-buffer.  Should allow
-;; face of nil for unfontified output.
 (defun proof-response-buffer-display (str &optional face)
   "Display STR with FACE in response buffer and return fontified STR."
+  (ugit str) ;; FIXME: debug!
   (let (start end)
     (with-current-buffer proof-response-buffer
       ;; da: I've moved newline before the string itself, to match
@@ -236,10 +316,14 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
       (newline)				
       (setq start (point))
       (insert str) 
-      (proof-x-symbol-decode-region start (point))
-      (setq end (point-max))
+      (setq end (proof-fontify-region start (point)))
+      ;; This is why we can't keep the buffer in font-lock
+      ;; minor mode: it destroys this hacky property as soon 
+      ;; as it's made!
       (if face (font-lock-append-text-property start end 'face face))
-      (buffer-substring start end))))
+      ;; This returns the decorated string, but it doesn't appear 
+      ;; decorated in the minibuffer, unfortunately.
+      (buffer-substring start (point-max)))))
 
 ;; FIXME da: this window dedicated stuff is a real pain and I've
 ;; spent ages inserting workarounds.  Why do we want it??
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el
index 767df53a..c18ea0a7 100644
--- a/isa/isa-syntax.el
+++ b/isa/isa-syntax.el
@@ -297,7 +297,7 @@
    (cons (concat "\353\\?'" isa-idx "\350") 'isabelle-tvar-name-face)
    (cons (concat "\354" isa-id "\350") 'isabelle-free-name-face)
    (cons (concat "\355" isa-id "\350") 'isabelle-bound-name-face)
-   (cons (concat "\356" "\\?" isa-idx "\350") 'isabelle-var-name-face)
+   (cons (concat "\356\\?" isa-idx "\350") 'isabelle-var-name-face)
    (cons (concat "\357" isa-idx "\350") 'proof-declaration-name-face)
    )
   "*Font-lock table for Isabelle terms.")