src/Pure/General/print_mode.ML
changeset 24613 bc889c3d55a3
parent 24603 425d6445cba6
child 24634 38db11874724
equal deleted inserted replaced
24612:d1b315bdb8d7 24613:bc889c3d55a3
     7 *)
     7 *)
     8 
     8 
     9 signature BASIC_PRINT_MODE =
     9 signature BASIC_PRINT_MODE =
    10 sig
    10 sig
    11   val print_mode: string list ref
    11   val print_mode: string list ref
       
    12   val print_mode_value: unit -> string list
    12   val print_mode_active: string -> bool
    13   val print_mode_active: string -> bool
    13 end;
    14 end;
    14 
    15 
    15 signature PRINT_MODE =
    16 signature PRINT_MODE =
    16 sig
    17 sig
    21 
    22 
    22 structure PrintMode: PRINT_MODE =
    23 structure PrintMode: PRINT_MODE =
    23 struct
    24 struct
    24 
    25 
    25 val print_mode = ref ([]: string list);
    26 val print_mode = ref ([]: string list);
    26 fun print_mode_active s = member (op =) (! print_mode) s;
    27 
       
    28 fun print_mode_value () = NAMED_CRITICAL "print_mode" (fn () => ! print_mode);
       
    29 fun print_mode_active s = member (op =) (print_mode_value ()) s;
    27 
    30 
    28 fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
    31 fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
    29   setmp print_mode (modes @ ! print_mode) f x);
    32   setmp print_mode (modes @ ! print_mode) f x);
    30 
    33 
    31 fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
    34 fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>