src/Pure/General/print_mode.ML
author wenzelm
Thu Jan 03 00:15:41 2008 +0100 (2008-01-03)
changeset 25798 1e6eafbb466f
parent 25734 b00b903ae8ae
child 28122 3d099ce624e7
permissions -rw-r--r--
setmp_thread_data;
wenzelm@23827
     1
(*  Title:      Pure/General/print_mode.ML
wenzelm@23827
     2
    ID:         $Id$
wenzelm@23827
     3
    Author:     Makarius
wenzelm@23827
     4
wenzelm@25734
     5
Generic print mode as thread-local value derived from global template;
wenzelm@25734
     6
provides implicit configuration for various output mechanisms.
wenzelm@23827
     7
*)
wenzelm@23827
     8
wenzelm@23934
     9
signature BASIC_PRINT_MODE =
wenzelm@23827
    10
sig
wenzelm@25734
    11
  val print_mode: string list ref            (*global template*)
wenzelm@25734
    12
  val print_mode_value: unit -> string list  (*thread-local value*)
wenzelm@25734
    13
  val print_mode_active: string -> bool      (*thread-local value*)
wenzelm@23827
    14
end;
wenzelm@23827
    15
wenzelm@23934
    16
signature PRINT_MODE =
wenzelm@23934
    17
sig
wenzelm@23934
    18
  include BASIC_PRINT_MODE
wenzelm@25118
    19
  val input: string
wenzelm@25118
    20
  val internal: string
wenzelm@24634
    21
  val setmp: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    22
  val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@25734
    23
  val closure: ('a -> 'b) -> 'a -> 'b
wenzelm@23934
    24
end;
wenzelm@23934
    25
wenzelm@23827
    26
structure PrintMode: PRINT_MODE =
wenzelm@23827
    27
struct
wenzelm@23827
    28
wenzelm@25118
    29
val input = "input";
wenzelm@25118
    30
val internal = "internal";
wenzelm@24613
    31
wenzelm@25118
    32
val print_mode = ref ([]: string list);
wenzelm@25734
    33
val tag = Universal.tag () : string list option Universal.tag;
wenzelm@25734
    34
wenzelm@25734
    35
fun print_mode_value () =
wenzelm@25734
    36
  let val modes =
wenzelm@25734
    37
    (case Multithreading.get_data tag of
wenzelm@25734
    38
      SOME (SOME modes) => modes
wenzelm@25734
    39
    | _ => NAMED_CRITICAL "print_mode" (fn () => ! print_mode))
wenzelm@25734
    40
  in subtract (op =) [input, internal] modes end;
wenzelm@25734
    41
wenzelm@25734
    42
fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
wenzelm@25118
    43
wenzelm@25734
    44
fun setmp modes f x =
wenzelm@25798
    45
  let val orig_modes = (case Multithreading.get_data tag of SOME (SOME ms) => SOME ms | _ => NONE)
wenzelm@25798
    46
  in setmp_thread_data tag orig_modes (SOME modes) f x end;
wenzelm@23827
    47
wenzelm@25734
    48
fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
wenzelm@25734
    49
fun closure f = with_modes [] f;
wenzelm@23934
    50
wenzelm@23827
    51
end;
wenzelm@23827
    52
wenzelm@23934
    53
structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
wenzelm@23934
    54
open BasicPrintMode;