src/Pure/General/print_mode.ML
author wenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 62889 99c7f31615c2
parent 62542 b27b7c2200b9
permissions -rw-r--r--
clarified modules;
tuned signature;
wenzelm@23827
     1
(*  Title:      Pure/General/print_mode.ML
wenzelm@23827
     2
    Author:     Makarius
wenzelm@23827
     3
wenzelm@25734
     4
Generic print mode as thread-local value derived from global template;
wenzelm@25734
     5
provides implicit configuration for various output mechanisms.
wenzelm@39124
     6
wenzelm@39124
     7
The special print mode "input" is never enabled for output.
wenzelm@23827
     8
*)
wenzelm@23827
     9
wenzelm@23934
    10
signature BASIC_PRINT_MODE =
wenzelm@23827
    11
sig
wenzelm@32738
    12
  val print_mode: string list Unsynchronized.ref  (*global template*)
wenzelm@32738
    13
  val print_mode_value: unit -> string list       (*thread-local value*)
wenzelm@32738
    14
  val print_mode_active: string -> bool           (*thread-local value*)
wenzelm@23827
    15
end;
wenzelm@23827
    16
wenzelm@23934
    17
signature PRINT_MODE =
wenzelm@23934
    18
sig
wenzelm@23934
    19
  include BASIC_PRINT_MODE
wenzelm@25118
    20
  val input: string
wenzelm@61957
    21
  val ASCII: string
wenzelm@25118
    22
  val internal: string
wenzelm@24634
    23
  val setmp: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    24
  val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@25734
    25
  val closure: ('a -> 'b) -> 'a -> 'b
wenzelm@62542
    26
  val add_modes: string list -> unit
wenzelm@23934
    27
end;
wenzelm@23934
    28
wenzelm@37146
    29
structure Print_Mode: PRINT_MODE =
wenzelm@23827
    30
struct
wenzelm@23827
    31
wenzelm@25118
    32
val input = "input";
wenzelm@61957
    33
val ASCII = "ASCII";
wenzelm@25118
    34
val internal = "internal";
wenzelm@24613
    35
wenzelm@32738
    36
val print_mode = Unsynchronized.ref ([]: string list);
wenzelm@62889
    37
val print_mode_var = Thread_Data.var () : string list Thread_Data.var;
wenzelm@25734
    38
wenzelm@25734
    39
fun print_mode_value () =
wenzelm@25734
    40
  let val modes =
wenzelm@62889
    41
    (case Thread_Data.get print_mode_var of
wenzelm@62889
    42
      SOME modes => modes
wenzelm@62889
    43
    | NONE => ! print_mode)
wenzelm@25734
    44
  in subtract (op =) [input, internal] modes end;
wenzelm@25734
    45
wenzelm@25734
    46
fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
wenzelm@25118
    47
wenzelm@62889
    48
fun setmp modes f x = Thread_Data.setmp print_mode_var (SOME modes) f x;
wenzelm@23827
    49
wenzelm@25734
    50
fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
wenzelm@25734
    51
fun closure f = with_modes [] f;
wenzelm@23934
    52
wenzelm@62542
    53
fun add_modes modes = Unsynchronized.change print_mode (append modes);
wenzelm@62542
    54
wenzelm@23827
    55
end;
wenzelm@23827
    56
wenzelm@37146
    57
structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
wenzelm@37146
    58
open Basic_Print_Mode;