src/Pure/General/print_mode.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 23827 0f0d1cf4992d
child 23934 79393cb9c0a6
permissions -rw-r--r--
tuned signature;
     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 PRINT_MODE =
    10 sig
    11   val print_mode: string list ref
    12   val print_mode_active: string -> bool
    13 end;
    14 
    15 structure PrintMode: PRINT_MODE =
    16 struct
    17 
    18 val print_mode = ref ([]: string list);
    19 fun print_mode_active s = member (op =) (! print_mode) s;
    20 
    21 end;
    22 
    23 open PrintMode;