blob: d1d0a0537b2e64f0de09cb573152e4800dfc60dc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
theory Test 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
|
