src/Pure/General/print_mode.ML
author wenzelm
Tue Dec 29 14:58:15 2015 +0100 (2015-12-29)
changeset 61957 301833d9013a
parent 39124 9bac2f4cfd6e
child 62542 b27b7c2200b9
permissions -rw-r--r--
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
uniform syntax for Pure.imp;
removed obsolete "HTML" syntax;
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@23934
    26
end;
wenzelm@23934
    27
wenzelm@37146
    28
structure Print_Mode: PRINT_MODE =
wenzelm@23827
    29
struct
wenzelm@23827
    30
wenzelm@25118
    31
val input = "input";
wenzelm@61957
    32
val ASCII = "ASCII";
wenzelm@25118
    33
val internal = "internal";
wenzelm@24613
    34
wenzelm@32738
    35
val print_mode = Unsynchronized.ref ([]: string list);
wenzelm@25734
    36
val tag = Universal.tag () : string list option Universal.tag;
wenzelm@25734
    37
wenzelm@25734
    38
fun print_mode_value () =
wenzelm@25734
    39
  let val modes =
wenzelm@28122
    40
    (case Thread.getLocal tag of
wenzelm@25734
    41
      SOME (SOME modes) => modes
wenzelm@33223
    42
    | _ => ! print_mode)
wenzelm@25734
    43
  in subtract (op =) [input, internal] modes end;
wenzelm@25734
    44
wenzelm@25734
    45
fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
wenzelm@25118
    46
wenzelm@25734
    47
fun setmp modes f x =
wenzelm@28122
    48
  let val orig_modes = (case Thread.getLocal tag of SOME (SOME ms) => SOME ms | _ => NONE)
wenzelm@25798
    49
  in setmp_thread_data tag orig_modes (SOME modes) f x end;
wenzelm@23827
    50
wenzelm@25734
    51
fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
wenzelm@25734
    52
fun closure f = with_modes [] f;
wenzelm@23934
    53
wenzelm@23827
    54
end;
wenzelm@23827
    55
wenzelm@37146
    56
structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
wenzelm@37146
    57
open Basic_Print_Mode;