equal
deleted
inserted
replaced
23 struct |
23 struct |
24 |
24 |
25 val print_mode = ref ([]: string list); |
25 val print_mode = ref ([]: string list); |
26 fun print_mode_active s = member (op =) (! print_mode) s; |
26 fun print_mode_active s = member (op =) (! print_mode) s; |
27 |
27 |
28 fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () => |
28 fun with_modes [] f x = f x |
29 setmp print_mode (modes @ ! print_mode) f x); |
29 | with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () => |
|
30 setmp print_mode (modes @ ! print_mode) f x); |
30 |
31 |
31 fun with_default f x = NAMED_CRITICAL "print_mode" (fn () => |
32 fun with_default f x = NAMED_CRITICAL "print_mode" (fn () => |
32 setmp print_mode [] f x); |
33 setmp print_mode [] f x); |
33 |
34 |
34 end; |
35 end; |