author | wenzelm |
Mon, 30 May 2022 10:52:00 +0200 | |
changeset 75489 | f08fd5048df3 |
parent 62889 | 99c7f31615c2 |
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. |
39124 | 6 |
|
7 |
The special print mode "input" is never enabled for output. |
|
23827 | 8 |
*) |
9 |
||
23934 | 10 |
signature BASIC_PRINT_MODE = |
23827 | 11 |
sig |
32738 | 12 |
val print_mode: string list Unsynchronized.ref (*global template*) |
13 |
val print_mode_value: unit -> string list (*thread-local value*) |
|
14 |
val print_mode_active: string -> bool (*thread-local value*) |
|
23827 | 15 |
end; |
16 |
||
23934 | 17 |
signature PRINT_MODE = |
18 |
sig |
|
19 |
include BASIC_PRINT_MODE |
|
25118
158149a6e95b
added input/internal, which are never active in print_mode_value;
wenzelm
parents:
24634
diff
changeset
|
20 |
val input: string |
61957
301833d9013a
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
39124
diff
changeset
|
21 |
val ASCII: string |
25118
158149a6e95b
added input/internal, which are never active in print_mode_value;
wenzelm
parents:
24634
diff
changeset
|
22 |
val internal: string |
24634 | 23 |
val setmp: string list -> ('a -> 'b) -> 'a -> 'b |
23934 | 24 |
val with_modes: string list -> ('a -> 'b) -> 'a -> 'b |
25734
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
25 |
val closure: ('a -> 'b) -> 'a -> 'b |
62542 | 26 |
val add_modes: string list -> unit |
23934 | 27 |
end; |
28 |
||
37146
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
33223
diff
changeset
|
29 |
structure Print_Mode: PRINT_MODE = |
23827 | 30 |
struct |
31 |
||
25118
158149a6e95b
added input/internal, which are never active in print_mode_value;
wenzelm
parents:
24634
diff
changeset
|
32 |
val input = "input"; |
61957
301833d9013a
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
39124
diff
changeset
|
33 |
val ASCII = "ASCII"; |
25118
158149a6e95b
added input/internal, which are never active in print_mode_value;
wenzelm
parents:
24634
diff
changeset
|
34 |
val internal = "internal"; |
24613 | 35 |
|
32738 | 36 |
val print_mode = Unsynchronized.ref ([]: string list); |
62889 | 37 |
val print_mode_var = Thread_Data.var () : string list Thread_Data.var; |
25734
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
38 |
|
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
39 |
fun print_mode_value () = |
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
40 |
let val modes = |
62889 | 41 |
(case Thread_Data.get print_mode_var of |
42 |
SOME modes => modes |
|
43 |
| NONE => ! print_mode) |
|
25734
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
44 |
in subtract (op =) [input, internal] modes end; |
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
45 |
|
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
46 |
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
|
47 |
|
62889 | 48 |
fun setmp modes f x = Thread_Data.setmp print_mode_var (SOME modes) f x; |
23827 | 49 |
|
25734
b00b903ae8ae
separated into global template vs. thread-local value;
wenzelm
parents:
25118
diff
changeset
|
50 |
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
|
51 |
fun closure f = with_modes [] f; |
23934 | 52 |
|
62542 | 53 |
fun add_modes modes = Unsynchronized.change print_mode (append modes); |
54 |
||
23827 | 55 |
end; |
56 |
||
37146
f652333bbf8e
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
wenzelm
parents:
33223
diff
changeset
|
57 |
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
|
58 |
open Basic_Print_Mode; |