src/Pure/General/print_mode.ML
author wenzelm
Mon Sep 17 16:36:43 2007 +0200 (2007-09-17)
changeset 24613 bc889c3d55a3
parent 24603 425d6445cba6
child 24634 38db11874724
permissions -rw-r--r--
added print_mode_value (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_value: unit -> string list
    13   val print_mode_active: string -> bool
    14 end;
    15 
    16 signature PRINT_MODE =
    17 sig
    18   include BASIC_PRINT_MODE
    19   val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
    20   val with_default: ('a -> 'b) -> 'a -> 'b
    21 end;
    22 
    23 structure PrintMode: PRINT_MODE =
    24 struct
    25 
    26 val print_mode = ref ([]: string list);
    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;
    30 
    31 fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
    32   setmp print_mode (modes @ ! print_mode) f x);
    33 
    34 fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
    35   setmp print_mode [] f x);
    36 
    37 end;
    38 
    39 structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
    40 open BasicPrintMode;