src/Pure/General/print_mode.ML
author wenzelm
Mon Aug 20 20:44:02 2007 +0200 (2007-08-20)
changeset 24362 a9fe7ed25fa4
parent 24058 81aafd465662
child 24603 425d6445cba6
permissions -rw-r--r--
with_modes []: non-critical;
     1 (*  Title:      Pure/General/print_mode.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Generic print mode -- implicit configuration for various output
     6 mechanisms.
     7 *)
     8 
     9 signature BASIC_PRINT_MODE =
    10 sig
    11   val print_mode: string list ref
    12   val print_mode_active: string -> bool
    13 end;
    14 
    15 signature PRINT_MODE =
    16 sig
    17   include BASIC_PRINT_MODE
    18   val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
    19   val with_default: ('a -> 'b) -> 'a -> 'b
    20 end;
    21 
    22 structure PrintMode: PRINT_MODE =
    23 struct
    24 
    25 val print_mode = ref ([]: string list);
    26 fun print_mode_active s = member (op =) (! print_mode) s;
    27 
    28 fun with_modes [] f x = f x
    29   | with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
    30       setmp print_mode (modes @ ! print_mode) f x);
    31 
    32 fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
    33   setmp print_mode [] f x);
    34 
    35 end;
    36 
    37 structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
    38 open BasicPrintMode;