equal
deleted
inserted
replaced
53 fun default_output s = (s, size s); |
53 fun default_output s = (s, size s); |
54 fun default_escape (s: output) = s; |
54 fun default_escape (s: output) = s; |
55 |
55 |
56 local |
56 local |
57 val default = {output = default_output, escape = default_escape}; |
57 val default = {output = default_output, escape = default_escape}; |
58 val modes = Unsynchronized.ref (Symtab.make [("", default)]); |
58 val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]); |
59 in |
59 in |
60 fun add_mode name output escape = CRITICAL (fn () => |
60 fun add_mode name output escape = |
61 Unsynchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}))); |
61 Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})); |
62 fun get_mode () = |
62 fun get_mode () = |
63 the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ())); |
63 the_default default |
|
64 (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); |
64 end; |
65 end; |
65 |
66 |
66 fun output_width x = #output (get_mode ()) x; |
67 fun output_width x = #output (get_mode ()) x; |
67 val output = #1 o output_width; |
68 val output = #1 o output_width; |
68 |
69 |