author | haftmann |
Mon, 30 Aug 2010 09:35:30 +0200 | |
changeset 38865 | 43c934dd4bc3 |
parent 37146 | f652333bbf8e |
child 39124 | 9bac2f4cfd6e |
permissions | -rw-r--r-- |
23827 | 1 |
(* Title: Pure/General/print_mode.ML |
2 |
Author: Makarius |
|
3 |
||
25734
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
4 |
Generic print mode as thread-local value derived from global template; |
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
5 |
provides implicit configuration for various output mechanisms. |
23827 | 6 |
*) |
7 |
||
23934 | 8 |
signature BASIC_PRINT_MODE = |
23827 | 9 |
sig |
32738 | 10 |
val print_mode: string list Unsynchronized.ref (*global template*) |
11 |
val print_mode_value: unit -> string list (*thread-local value*) |
|
12 |
val print_mode_active: string -> bool (*thread-local value*) |
|
23827 | 13 |
end; |
14 |
||
23934 | 15 |
signature PRINT_MODE = |
16 |
sig |
|
17 |
include BASIC_PRINT_MODE |
|
25118
158149a6e95b
added input/internal, which are never active in print_mode_value;
wenzelm
parents:
24634
diff
changeset
|
18 |
val input: string |
158149a6e95b
added input/internal, which are never active in print_mode_value;
wenzelm
parents:
24634
diff
changeset
|
19 |
val internal: string |
24634 | 20 |
val setmp: string list -> ('a -> 'b) -> 'a -> 'b |
23934 | 21 |
val with_modes: string list -> ('a -> 'b) -> 'a -> 'b |
25734
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
22 |
val closure: ('a -> 'b) -> 'a -> 'b |
23934 | 23 |
end; |
24 |
||
37146
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
33223
diff
changeset
|
25 |
structure Print_Mode: PRINT_MODE = |
23827 | 26 |
struct |
27 |
||
25118
158149a6e95b
added input/internal, which are never active in print_mode_value;
wenzelm
parents:
24634
diff
changeset
|
28 |
val input = "input"; |
158149a6e95b
added input/internal, which are never active in print_mode_value;
wenzelm
parents:
24634
diff
changeset
|
29 |
val internal = "internal"; |
24613 | 30 |
|
32738 | 31 |
val print_mode = Unsynchronized.ref ([]: string list); |
25734
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
32 |
val tag = Universal.tag () : string list option Universal.tag; |
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
33 |
|
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
34 |
fun print_mode_value () = |
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
35 |
let val modes = |
28122 | 36 |
(case Thread.getLocal tag of |
25734
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
37 |
SOME (SOME modes) => modes |
33223 | 38 |
| _ => ! print_mode) |
25734
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
39 |
in subtract (op =) [input, internal] modes end; |
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
40 |
|
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
41 |
fun print_mode_active mode = member (op =) (print_mode_value ()) mode; |
25118
158149a6e95b
added input/internal, which are never active in print_mode_value;
wenzelm
parents:
24634
diff
changeset
|
42 |
|
25734
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
43 |
fun setmp modes f x = |
28122 | 44 |
let val orig_modes = (case Thread.getLocal tag of SOME (SOME ms) => SOME ms | _ => NONE) |
25798 | 45 |
in setmp_thread_data tag orig_modes (SOME modes) f x end; |
23827 | 46 |
|
25734
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
47 |
fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x; |
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
48 |
fun closure f = with_modes [] f; |
23934 | 49 |
|
23827 | 50 |
end; |
51 |
||
37146
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
33223
diff
changeset
|
52 |
structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode; |
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
33223
diff
changeset
|
53 |
open Basic_Print_Mode; |