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 [] f x = f x |
28 fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () => |
29 | with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () => |
29 setmp print_mode (modes @ ! print_mode) f x); |
30 setmp print_mode (modes @ ! print_mode) f x); |
|
31 |
30 |
32 fun with_default f x = NAMED_CRITICAL "print_mode" (fn () => |
31 fun with_default f x = NAMED_CRITICAL "print_mode" (fn () => |
33 setmp print_mode [] f x); |
32 setmp print_mode [] f x); |
34 |
33 |
35 end; |
34 end; |