src/Pure/General/print_mode.ML
author wenzelm
Tue Sep 29 11:49:22 2009 +0200 (2009-09-29)
changeset 32738 15bb09ca0378
parent 29606 fedb8be05f24
child 33223 d27956b4d3b4
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
     1 (*  Title:      Pure/General/print_mode.ML
     2     Author:     Makarius
     3 
     4 Generic print mode as thread-local value derived from global template;
     5 provides implicit configuration for various output mechanisms.
     6 *)
     7 
     8 signature BASIC_PRINT_MODE =
     9 sig
    10   val print_mode: string list Unsynchronized.ref  (*global template*)
    11   val print_mode_value: unit -> string list       (*thread-local value*)
    12   val print_mode_active: string -> bool           (*thread-local value*)
    13 end;
    14 
    15 signature PRINT_MODE =
    16 sig
    17   include BASIC_PRINT_MODE
    18   val input: string
    19   val internal: string
    20   val setmp: string list -> ('a -> 'b) -> 'a -> 'b
    21   val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
    22   val closure: ('a -> 'b) -> 'a -> 'b
    23 end;
    24 
    25 structure PrintMode: PRINT_MODE =
    26 struct
    27 
    28 val input = "input";
    29 val internal = "internal";
    30 
    31 val print_mode = Unsynchronized.ref ([]: string list);
    32 val tag = Universal.tag () : string list option Universal.tag;
    33 
    34 fun print_mode_value () =
    35   let val modes =
    36     (case Thread.getLocal tag of
    37       SOME (SOME modes) => modes
    38     | _ => NAMED_CRITICAL "print_mode" (fn () => ! print_mode))
    39   in subtract (op =) [input, internal] modes end;
    40 
    41 fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
    42 
    43 fun setmp modes f x =
    44   let val orig_modes = (case Thread.getLocal tag of SOME (SOME ms) => SOME ms | _ => NONE)
    45   in setmp_thread_data tag orig_modes (SOME modes) f x end;
    46 
    47 fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
    48 fun closure f = with_modes [] f;
    49 
    50 end;
    51 
    52 structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
    53 open BasicPrintMode;