Special markup not processed in minibuffer messages (warnings etc.)

[Makarius]

XEmacs 21.4.21 on Ubuntu Linux 8.04; Isabelle2008.

The special markup (for terms etc.) is not processed in minibuffer messages. For example:

ML_command {* warning (Syntax.string_of_typ @{context} @{typ 'a}) *}

Here the decoration for 'a shows up as funny control characters, instead of proper font-lock colouring.

[Makarius]

The same happens for x-symbols, displaying only \<lambda> in the minibuffer instead of λ.

[Generic Isabelle user]

Proper colouring is also lost when one highlights parts of a processed proof script (for example "proof with point in region").

[David Aspinall]

Closing because current PG CVS head works on 21.5 (beta28) \"fuki\" XEmacs Lucid and Emacs CVS version.

Test added in trac/trac-206.thy, please reopen if current PG CVS head fails on a version of Emacs that must be supported. (Note: XEmacs is deprecated).

[Makarius]

It also fails on GNU Emacs 22.1.1, which is the one of Ubuntu Linux 8.04 LTS or SuSE 10.3 (which are not that old).

One could consider giving up fontified minibuffer output altogether, e.g. like this at the end of proof-shell-message:

     (t
      ;; CASE everything else.  We're about to display a message.  
      ;; Clear the response buffer this time, but not next, leave window.
      (pg-response-maybe-erase nil nil)
      (let ((stripped (pg-remove-specials-in-string message)))
	;; Display first chunk of output in minibuffer.
	;; Maybe this should be configurable, it can get noisy.
	(proof-shell-message 
	 (substring stripped 0 (or (string-match "\n" stripped)
				   (min (length stripped) 75))))
	(pg-response-display-with-face 
	 (proof-shell-strip-eager-annotations message)
	 'proof-eager-annotation-face)))))

[David Aspinall]

OK: the plain output is now sent to the minibuffer.

Markup is tricky: we'd have to fontify specially (output buffer may not even be displayed), and #266 shows you that could involve fontifying a lot of text just to strip off the first line to show in the minibuffer.

We could investigate more efficient fontification which works on unclosed text (i.e., does not need </highlight> anchors). But I think we might instead simply give up the minibuffer display. Would everyone hate that?