src/Pure/General/print_mode.ML
author wenzelm
Sun Jul 29 17:28:55 2007 +0200 (2007-07-29)
changeset 24058 81aafd465662
parent 23934 79393cb9c0a6
child 24362 a9fe7ed25fa4
permissions -rw-r--r--
NAMED_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 modes f x = NAMED_CRITICAL "print_mode" (fn () =>
    29   setmp print_mode (modes @ ! print_mode) f x);
    30 
    31 fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
    32   setmp print_mode [] f x);
    33 
    34 end;
    35 
    36 structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
    37 open BasicPrintMode;