src/Pure/General/print_mode.ML
author wenzelm
Sat Oct 20 18:54:31 2007 +0200 (2007-10-20)
changeset 25118 158149a6e95b
parent 24634 38db11874724
child 25734 b00b903ae8ae
permissions -rw-r--r--
added input/internal, which are never active in print_mode_value;
     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 input: string
    20   val internal: string
    21   val setmp: string list -> ('a -> 'b) -> 'a -> 'b
    22   val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
    23 end;
    24 
    25 structure PrintMode: PRINT_MODE =
    26 struct
    27 
    28 val input = "input";
    29 val internal = "internal";
    30 
    31 val print_mode = ref ([]: string list);
    32 fun get_mode () = subtract (op =) [input, internal] (! print_mode);
    33 
    34 fun print_mode_value () = NAMED_CRITICAL "print_mode" get_mode;
    35 fun print_mode_active s = member (op =) (print_mode_value ()) s;
    36 
    37 fun setmp modes f x = NAMED_CRITICAL "print_mode" (fn () => Library.setmp print_mode modes f x);
    38 fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () => setmp (modes @ ! print_mode) f x);
    39 
    40 end;
    41 
    42 structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
    43 open BasicPrintMode;