src/Pure/General/print_mode.ML
author wenzelm
Mon Jul 23 16:45:02 2007 +0200 (2007-07-23)
changeset 23934 79393cb9c0a6
parent 23827 0f0d1cf4992d
child 24058 81aafd465662
permissions -rw-r--r--
added with_modes, with_default;
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@23934
     9
signature BASIC_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@23934
    15
signature PRINT_MODE =
wenzelm@23934
    16
sig
wenzelm@23934
    17
  include BASIC_PRINT_MODE
wenzelm@23934
    18
  val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    19
  val with_default: ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    20
end;
wenzelm@23934
    21
wenzelm@23827
    22
structure PrintMode: PRINT_MODE =
wenzelm@23827
    23
struct
wenzelm@23827
    24
wenzelm@23827
    25
val print_mode = ref ([]: string list);
wenzelm@23827
    26
fun print_mode_active s = member (op =) (! print_mode) s;
wenzelm@23827
    27
wenzelm@23934
    28
fun with_modes modes f x = CRITICAL (fn () =>
wenzelm@23934
    29
  setmp print_mode (modes @ ! print_mode) f x);
wenzelm@23934
    30
wenzelm@23934
    31
fun with_default f x = setmp print_mode [] f x;
wenzelm@23934
    32
wenzelm@23827
    33
end;
wenzelm@23827
    34
wenzelm@23934
    35
structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
wenzelm@23934
    36
open BasicPrintMode;