blob: 7c0b26c8c347d26d9d9b67adbca68cc90b2dfa70 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(* see trac #206 *)
theory Trac206 imports Main begin
(* The special markup (for terms etc.) is not processed in minibuffer
messages. For example: *)
ML_command {* warning (Syntax.string_of_typ @{context} @{typ 'a}) *}
term "\<lambda> x. x"
(* Here the decoration for 'a shows up as funny control characters,
instead of proper font-lock colouring. *)
end
|
