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;
wenzelm@23827
     1
(*  Title:      Pure/General/print_mode.ML
wenzelm@23827
     2
    ID:         $Id$
wenzelm@23827
     3
    Author:     Makarius
wenzelm@23827
     4
wenzelm@23827
     5
Generic print mode -- implicit configuration for various output
wenzelm@23827
     6
mechanisms.
wenzelm@23827
     7
*)
wenzelm@23827
     8
wenzelm@23827
     9
signature PRINT_MODE =
wenzelm@23827
    10
sig
wenzelm@23827
    11
  val print_mode: string list ref
wenzelm@23827
    12
  val print_mode_active: string -> bool
wenzelm@23827
    13
end;
wenzelm@23827
    14
wenzelm@23827
    15
structure PrintMode: PRINT_MODE =
wenzelm@23827
    16
struct
wenzelm@23827
    17
wenzelm@23827
    18
val print_mode = ref ([]: string list);
wenzelm@23827
    19
fun print_mode_active s = member (op =) (! print_mode) s;
wenzelm@23827
    20
wenzelm@23827
    21
end;
wenzelm@23827
    22
wenzelm@23827
    23
open PrintMode;