src/Pure/General/print_mode.ML
author wenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 62889 99c7f31615c2
parent 62542 b27b7c2200b9
permissions -rw-r--r--
clarified modules;
tuned signature;
     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 The special print mode "input" is never enabled for output.
     8 *)
     9 
    10 signature BASIC_PRINT_MODE =
    11 sig
    12   val print_mode: string list Unsynchronized.ref  (*global template*)
    13   val print_mode_value: unit -> string list       (*thread-local value*)
    14   val print_mode_active: string -> bool           (*thread-local value*)
    15 end;
    16 
    17 signature PRINT_MODE =
    18 sig
    19   include BASIC_PRINT_MODE
    20   val input: string
    21   val ASCII: string
    22   val internal: string
    23   val setmp: string list -> ('a -> 'b) -> 'a -> 'b
    24   val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
    25   val closure: ('a -> 'b) -> 'a -> 'b
    26   val add_modes: string list -> unit
    27 end;
    28 
    29 structure Print_Mode: PRINT_MODE =
    30 struct
    31 
    32 val input = "input";
    33 val ASCII = "ASCII";
    34 val internal = "internal";
    35 
    36 val print_mode = Unsynchronized.ref ([]: string list);
    37 val print_mode_var = Thread_Data.var () : string list Thread_Data.var;
    38 
    39 fun print_mode_value () =
    40   let val modes =
    41     (case Thread_Data.get print_mode_var of
    42       SOME modes => modes
    43     | NONE => ! print_mode)
    44   in subtract (op =) [input, internal] modes end;
    45 
    46 fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
    47 
    48 fun setmp modes f x = Thread_Data.setmp print_mode_var (SOME modes) f x;
    49 
    50 fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
    51 fun closure f = with_modes [] f;
    52 
    53 fun add_modes modes = Unsynchronized.change print_mode (append modes);
    54 
    55 end;
    56 
    57 structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
    58 open Basic_Print_Mode;