src/Pure/General/print_mode.ML
author wenzelm
Mon Aug 20 20:44:02 2007 +0200 (2007-08-20)
changeset 24362 a9fe7ed25fa4
parent 24058 81aafd465662
child 24603 425d6445cba6
permissions -rw-r--r--
with_modes []: non-critical;
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@24362
    28
fun with_modes [] f x = f x
wenzelm@24362
    29
  | with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () =>
wenzelm@24362
    30
      setmp print_mode (modes @ ! print_mode) f x);
wenzelm@23934
    31
wenzelm@24058
    32
fun with_default f x = NAMED_CRITICAL "print_mode" (fn () =>
wenzelm@24058
    33
  setmp print_mode [] f x);
wenzelm@23934
    34
wenzelm@23827
    35
end;
wenzelm@23827
    36
wenzelm@23934
    37
structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
wenzelm@23934
    38
open BasicPrintMode;