# HG changeset patch
# User wenzelm
# Date 1198181521 -3600
# Node ID b00b903ae8aee4a33eb54bd0785fa8764b566769
# Parent  8722d68471ff0a6e1ace5d71e1fd7e61a59d2e62
separated into global template vs. thread-local value;
made setmp thread-local (non-critical);
added closure;

diff -r 8722d68471ff -r b00b903ae8ae src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Thu Dec 20 21:12:00 2007 +0100
+++ b/src/Pure/General/print_mode.ML	Thu Dec 20 21:12:01 2007 +0100
@@ -2,15 +2,15 @@
     ID:         $Id$
     Author:     Makarius
 
-Generic print mode -- implicit configuration for various output
-mechanisms.
+Generic print mode as thread-local value derived from global template;
+provides implicit configuration for various output mechanisms.
 *)
 
 signature BASIC_PRINT_MODE =
 sig
-  val print_mode: string list ref
-  val print_mode_value: unit -> string list
-  val print_mode_active: string -> bool
+  val print_mode: string list ref            (*global template*)
+  val print_mode_value: unit -> string list  (*thread-local value*)
+  val print_mode_active: string -> bool      (*thread-local value*)
 end;
 
 signature PRINT_MODE =
@@ -20,6 +20,7 @@
   val internal: string
   val setmp: string list -> ('a -> 'b) -> 'a -> 'b
   val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
+  val closure: ('a -> 'b) -> 'a -> 'b
 end;
 
 structure PrintMode: PRINT_MODE =
@@ -29,13 +30,30 @@
 val internal = "internal";
 
 val print_mode = ref ([]: string list);
-fun get_mode () = subtract (op =) [input, internal] (! print_mode);
+val tag = Universal.tag () : string list option Universal.tag;
+
+fun print_mode_value () =
+  let val modes =
+    (case Multithreading.get_data tag of
+      SOME (SOME modes) => modes
+    | _ => NAMED_CRITICAL "print_mode" (fn () => ! print_mode))
+  in subtract (op =) [input, internal] modes end;
+
+fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
 
-fun print_mode_value () = NAMED_CRITICAL "print_mode" get_mode;
-fun print_mode_active s = member (op =) (print_mode_value ()) s;
+fun setmp modes f x =
+  let
+    val orig_data =
+      (case Multithreading.get_data tag of
+        SOME (SOME orig_modes) => SOME orig_modes
+      | _ => NONE);
+    val _ = Multithreading.put_data (tag, SOME modes);
+    val result = Exn.capture f x;
+    val _ = Multithreading.put_data (tag, orig_data);
+  in Exn.release result end;
 
-fun setmp modes f x = NAMED_CRITICAL "print_mode" (fn () => Library.setmp print_mode modes f x);
-fun with_modes modes f x = NAMED_CRITICAL "print_mode" (fn () => setmp (modes @ ! print_mode) f x);
+fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
+fun closure f = with_modes [] f;
 
 end;