equal
deleted
inserted
replaced
376 val no_output = ("", ""); |
376 val no_output = ("", ""); |
377 fun default_output (_: T) = no_output; |
377 fun default_output (_: T) = no_output; |
378 |
378 |
379 local |
379 local |
380 val default = {output = default_output}; |
380 val default = {output = default_output}; |
381 val modes = Unsynchronized.ref (Symtab.make [("", default)]); |
381 val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]); |
382 in |
382 in |
383 fun add_mode name output = CRITICAL (fn () => |
383 fun add_mode name output = |
384 Unsynchronized.change modes (Symtab.update_new (name, {output = output}))); |
384 Synchronized.change modes (Symtab.update_new (name, {output = output})); |
385 fun get_mode () = |
385 fun get_mode () = |
386 the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ())); |
386 the_default default |
|
387 (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ())); |
387 end; |
388 end; |
388 |
389 |
389 fun output m = if is_empty m then no_output else #output (get_mode ()) m; |
390 fun output m = if is_empty m then no_output else #output (get_mode ()) m; |
390 |
391 |
391 val enclose = output #-> Library.enclose; |
392 val enclose = output #-> Library.enclose; |