equal
deleted
inserted
replaced
73 |
73 |
74 fun default_indent (_: string) = Symbol.spaces; |
74 fun default_indent (_: string) = Symbol.spaces; |
75 |
75 |
76 local |
76 local |
77 val default = {indent = default_indent}; |
77 val default = {indent = default_indent}; |
78 val modes = Unsynchronized.ref (Symtab.make [("", default)]); |
78 val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]); |
79 in |
79 in |
80 fun add_mode name indent = CRITICAL (fn () => |
80 fun add_mode name indent = |
81 Unsynchronized.change modes (Symtab.update_new (name, {indent = indent}))); |
81 Synchronized.change modes (Symtab.update_new (name, {indent = indent})); |
82 fun get_mode () = |
82 fun get_mode () = |
83 the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ())); |
83 the_default default |
|
84 (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); |
84 end; |
85 end; |
85 |
86 |
86 fun mode_indent x y = #indent (get_mode ()) x y; |
87 fun mode_indent x y = #indent (get_mode ()) x y; |
87 |
88 |
88 val output_spaces = Output.output o Symbol.spaces; |
89 val output_spaces = Output.output o Symbol.spaces; |