src/Pure/General/print_mode.ML
author wenzelm
Thu Dec 20 21:12:01 2007 +0100 (2007-12-20)
changeset 25734 b00b903ae8ae
parent 25118 158149a6e95b
child 25798 1e6eafbb466f
permissions -rw-r--r--
separated into global template vs. thread-local value;
made setmp thread-local (non-critical);
added closure;
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@25734
    45
  let
wenzelm@25734
    46
    val orig_data =
wenzelm@25734
    47
      (case Multithreading.get_data tag of
wenzelm@25734
    48
        SOME (SOME orig_modes) => SOME orig_modes
wenzelm@25734
    49
      | _ => NONE);
wenzelm@25734
    50
    val _ = Multithreading.put_data (tag, SOME modes);
wenzelm@25734
    51
    val result = Exn.capture f x;
wenzelm@25734
    52
    val _ = Multithreading.put_data (tag, orig_data);
wenzelm@25734
    53
  in Exn.release result end;
wenzelm@23827
    54
wenzelm@25734
    55
fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
wenzelm@25734
    56
fun closure f = with_modes [] f;
wenzelm@23934
    57
wenzelm@23827
    58
end;
wenzelm@23827
    59
wenzelm@23934
    60
structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
wenzelm@23934
    61
open BasicPrintMode;