src/Pure/General/print_mode.ML
author wenzelm
Thu May 27 18:10:37 2010 +0200 (2010-05-27)
changeset 37146 f652333bbf8e
parent 33223 d27956b4d3b4
child 39124 9bac2f4cfd6e
permissions -rw-r--r--
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
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@23827
     6
*)
wenzelm@23827
     7
wenzelm@23934
     8
signature BASIC_PRINT_MODE =
wenzelm@23827
     9
sig
wenzelm@32738
    10
  val print_mode: string list Unsynchronized.ref  (*global template*)
wenzelm@32738
    11
  val print_mode_value: unit -> string list       (*thread-local value*)
wenzelm@32738
    12
  val print_mode_active: string -> bool           (*thread-local value*)
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@25118
    18
  val input: string
wenzelm@25118
    19
  val internal: string
wenzelm@24634
    20
  val setmp: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    21
  val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@25734
    22
  val closure: ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    23
end;
wenzelm@23934
    24
wenzelm@37146
    25
structure Print_Mode: PRINT_MODE =
wenzelm@23827
    26
struct
wenzelm@23827
    27
wenzelm@25118
    28
val input = "input";
wenzelm@25118
    29
val internal = "internal";
wenzelm@24613
    30
wenzelm@32738
    31
val print_mode = Unsynchronized.ref ([]: string list);
wenzelm@25734
    32
val tag = Universal.tag () : string list option Universal.tag;
wenzelm@25734
    33
wenzelm@25734
    34
fun print_mode_value () =
wenzelm@25734
    35
  let val modes =
wenzelm@28122
    36
    (case Thread.getLocal tag of
wenzelm@25734
    37
      SOME (SOME modes) => modes
wenzelm@33223
    38
    | _ => ! print_mode)
wenzelm@25734
    39
  in subtract (op =) [input, internal] modes end;
wenzelm@25734
    40
wenzelm@25734
    41
fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
wenzelm@25118
    42
wenzelm@25734
    43
fun setmp modes f x =
wenzelm@28122
    44
  let val orig_modes = (case Thread.getLocal tag of SOME (SOME ms) => SOME ms | _ => NONE)
wenzelm@25798
    45
  in setmp_thread_data tag orig_modes (SOME modes) f x end;
wenzelm@23827
    46
wenzelm@25734
    47
fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
wenzelm@25734
    48
fun closure f = with_modes [] f;
wenzelm@23934
    49
wenzelm@23827
    50
end;
wenzelm@23827
    51
wenzelm@37146
    52
structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
wenzelm@37146
    53
open Basic_Print_Mode;