src/Pure/General/print_mode.ML
author wenzelm
Fri Sep 03 20:39:38 2010 +0200 (2010-09-03)
changeset 39124 9bac2f4cfd6e
parent 37146 f652333bbf8e
child 61957 301833d9013a
permissions -rw-r--r--
tuned comment;
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@25118
    21
  val internal: string
wenzelm@24634
    22
  val setmp: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    23
  val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@25734
    24
  val closure: ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    25
end;
wenzelm@23934
    26
wenzelm@37146
    27
structure Print_Mode: PRINT_MODE =
wenzelm@23827
    28
struct
wenzelm@23827
    29
wenzelm@25118
    30
val input = "input";
wenzelm@25118
    31
val internal = "internal";
wenzelm@24613
    32
wenzelm@32738
    33
val print_mode = Unsynchronized.ref ([]: string list);
wenzelm@25734
    34
val tag = Universal.tag () : string list option Universal.tag;
wenzelm@25734
    35
wenzelm@25734
    36
fun print_mode_value () =
wenzelm@25734
    37
  let val modes =
wenzelm@28122
    38
    (case Thread.getLocal tag of
wenzelm@25734
    39
      SOME (SOME modes) => modes
wenzelm@33223
    40
    | _ => ! print_mode)
wenzelm@25734
    41
  in subtract (op =) [input, internal] modes end;
wenzelm@25734
    42
wenzelm@25734
    43
fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
wenzelm@25118
    44
wenzelm@25734
    45
fun setmp modes f x =
wenzelm@28122
    46
  let val orig_modes = (case Thread.getLocal tag of SOME (SOME ms) => SOME ms | _ => NONE)
wenzelm@25798
    47
  in setmp_thread_data tag orig_modes (SOME modes) f x end;
wenzelm@23827
    48
wenzelm@25734
    49
fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
wenzelm@25734
    50
fun closure f = with_modes [] f;
wenzelm@23934
    51
wenzelm@23827
    52
end;
wenzelm@23827
    53
wenzelm@37146
    54
structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
wenzelm@37146
    55
open Basic_Print_Mode;