# HG changeset patch
# User wenzelm
# Date 1459953213 -7200
# Node ID 99c7f31615c2b0978298d36d1522838706c1ba28
# Parent  64f44d7279e599a8e4d61a113934714717683c04
clarified modules;
tuned signature;

diff -r 64f44d7279e5 -r 99c7f31615c2 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -279,7 +279,8 @@
                 let
                   val output_value = the_default "NONE"
                     (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
-                  val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
+                  val ml_code =
+                    "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^ put_ml
                     ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))";
                   val ctxt' = ctxt
                     |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/Concurrent/future.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -58,10 +58,10 @@
 (* identifiers *)
 
 local
-  val tag = Universal.tag () : task option Universal.tag;
+  val worker_task_var = Thread_Data.var () : task Thread_Data.var;
 in
-  fun worker_task () = the_default NONE (Thread.getLocal tag);
-  fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x;
+  fun worker_task () = Thread_Data.get worker_task_var;
+  fun setmp_worker_task task f x = Thread_Data.setmp worker_task_var (SOME task) f x;
 end;
 
 val worker_group = Option.map Task_Queue.group_of_task o worker_task;
@@ -432,14 +432,14 @@
   let
     val result = Single_Assignment.var "future" : 'a result;
     val pos = Position.thread_data ();
-    val context = Context.thread_data ();
+    val context = Context.get_generic_context ();
     fun job ok =
       let
         val res =
           if ok then
             Exn.capture (fn () =>
               Multithreading.with_attributes atts (fn _ =>
-                (Position.setmp_thread_data pos o Context.setmp_thread_data context) e ())) ()
+                (Position.setmp_thread_data pos o Context.setmp_generic_context context) e ())) ()
           else Exn.interrupt_exn;
       in assign_result group result (identify_result pos res) end;
   in (result, job) end;
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/Concurrent/standard_thread.ML
--- a/src/Pure/Concurrent/standard_thread.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/Concurrent/standard_thread.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -27,11 +27,11 @@
 (* unique name *)
 
 local
-  val tag = Universal.tag () : string Universal.tag;
+  val name_var = Thread_Data.var () : string Thread_Data.var;
   val count = Counter.make ();
 in
 
-fun get_name () = Thread.getLocal tag;
+fun get_name () = Thread_Data.get name_var;
 
 fun the_name () =
   (case get_name () of
@@ -39,7 +39,7 @@
   | SOME name => name);
 
 fun set_name base =
-  Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
+  Thread_Data.put name_var (SOME (base ^ "/" ^ string_of_int (count ())));
 
 end;
 
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/Concurrent/thread_data.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/thread_data.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -0,0 +1,42 @@
+(*  Title:      Pure/Concurrent/thread_data.ML
+    Author:     Makarius
+
+Thread-local data -- raw version without context management.
+*)
+
+signature THREAD_DATA =
+sig
+  type 'a var
+  val var: unit -> 'a var
+  val get: 'a var -> 'a option
+  val put: 'a var -> 'a option -> unit
+  val setmp: 'a var -> 'a option -> ('b -> 'c) -> 'b -> 'c
+end;
+
+structure Thread_Data: THREAD_DATA =
+struct
+
+abstype 'a var = Var of 'a option Universal.tag
+with
+
+fun var () : 'a var = Var (Universal.tag ());
+
+fun get (Var tag) =
+  (case Thread.getLocal tag of
+    SOME data => data
+  | NONE => NONE);
+
+fun put (Var tag) data = Thread.setLocal (tag, data);
+
+fun setmp v data f x =
+  uninterruptible (fn restore_attributes => fn () =>
+    let
+      val orig_data = get v;
+      val _ = put v data;
+      val result = Exn.capture (restore_attributes f) x;
+      val _ = put v orig_data;
+    in Exn.release result end) ();
+
+end;
+
+end;
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/General/position.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -243,13 +243,9 @@
 
 (* thread data *)
 
-local val tag = Universal.tag () : T Universal.tag in
-
-fun thread_data () = the_default none (Thread.getLocal tag);
-
-fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos;
-
-end;
+val thread_data_var = Thread_Data.var () : T Thread_Data.var;
+fun thread_data () = the_default none (Thread_Data.get thread_data_var);
+fun setmp_thread_data pos = Thread_Data.setmp thread_data_var (SOME pos);
 
 fun default pos =
   if pos = none then (false, thread_data ())
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/General/print_mode.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -34,20 +34,18 @@
 val internal = "internal";
 
 val print_mode = Unsynchronized.ref ([]: string list);
-val tag = Universal.tag () : string list option Universal.tag;
+val print_mode_var = Thread_Data.var () : string list Thread_Data.var;
 
 fun print_mode_value () =
   let val modes =
-    (case Thread.getLocal tag of
-      SOME (SOME modes) => modes
-    | _ => ! print_mode)
+    (case Thread_Data.get print_mode_var of
+      SOME modes => modes
+    | NONE => ! print_mode)
   in subtract (op =) [input, internal] modes end;
 
 fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
 
-fun setmp modes f x =
-  let val orig_modes = (case Thread.getLocal tag of SOME (SOME ms) => SOME ms | _ => NONE)
-  in setmp_thread_data tag orig_modes (SOME modes) f x end;
+fun setmp modes f x = Thread_Data.setmp print_mode_var (SOME modes) f x;
 
 fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
 fun closure f = with_modes [] f;
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/Isar/method.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -355,8 +355,7 @@
              ML_Lex.read_source false source);
         val tac = the_tactic context';
       in
-        fn phi =>
-          set_tactic (fn _ => Context.setmp_thread_data (SOME context) (tac phi))
+        fn phi => set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi))
       end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context))));
 
 
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -39,7 +39,7 @@
   else Pretty.str "<context>");
 
 fun default_context mk_thy =
-  (case Context.thread_data () of
+  (case Context.get_generic_context () of
     SOME (Context.Proof ctxt) => ctxt
   | SOME (Context.Theory thy) =>
       (case try Syntax.init_pretty_global thy of
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/Isar/runtime.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -54,7 +54,7 @@
   | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
 
 fun thread_context exn =
-  exn_context (Option.map Context.proof_of (Context.thread_data ())) exn;
+  exn_context (Option.map Context.proof_of (Context.get_generic_context ())) exn;
 
 
 (* exn_message *)
@@ -202,7 +202,7 @@
     else
       let
         val opt_ctxt =
-          (case Context.thread_data () of
+          (case Context.get_generic_context () of
             NONE => NONE
           | SOME context => try Context.proof_of context);
         val _ = output_exn (exn_context opt_ctxt exn);
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -574,7 +574,7 @@
 fun transition int tr st =
   let
     val (st', opt_err) =
-      Context.setmp_thread_data (try (Context.Proof o presentation_context_of) st)
+      Context.setmp_generic_context (try (Context.Proof o presentation_context_of) st)
         (fn () => app int tr st) ();
     val opt_err' = opt_err |> Option.map
       (fn Runtime.EXCURSION_FAIL exn_info => exn_info
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/ML/exn_debugger.ML
--- a/src/Pure/ML/exn_debugger.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/ML/exn_debugger.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -15,28 +15,24 @@
 
 (* thread data *)
 
-local
-  val tag =
-    Universal.tag () : ((string * ML_Compiler0.polyml_location) * exn) list option Universal.tag;
-in
+val trace_var =
+  Thread_Data.var () : ((string * ML_Compiler0.polyml_location) * exn) list Thread_Data.var;
 
-fun start_trace () = Thread.setLocal (tag, SOME []);
+fun start_trace () = Thread_Data.put trace_var (SOME []);
 
 fun update_trace entry exn =
-  (case Thread.getLocal tag of
-    SOME (SOME trace) => Thread.setLocal (tag, SOME ((entry, exn) :: trace))
-  | _ => ());
+  (case Thread_Data.get trace_var of
+    SOME trace => Thread_Data.put trace_var (SOME ((entry, exn) :: trace))
+  | NONE => ());
 
 fun stop_trace () =
   let
-    val trace = (case Thread.getLocal tag of SOME (SOME trace) => trace | _ => []);
-    val _ = Thread.setLocal (tag, NONE);
+    val trace = the_default [] (Thread_Data.get trace_var);
+    val _ = Thread_Data.put trace_var NONE;
   in trace end;
 
 val _ = ML_Debugger.on_exit_exception (SOME update_trace);
 
-end;
-
 
 (* capture exception trace *)
 
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -52,7 +52,7 @@
 fun report_parse_tree redirect depth space parse_tree =
   let
     val is_visible =
-      (case Context.thread_data () of
+      (case Context.get_generic_context () of
         SOME context => Context_Position.is_visible_generic context
       | NONE => true);
     fun is_reported pos = is_visible andalso Position.is_reported pos;
@@ -135,7 +135,7 @@
     val all_breakpoints = rev (breakpoints_tree parse_tree []);
     val _ = Position.reports (map #1 all_breakpoints);
     val _ =
-      if is_some (Context.thread_data ()) then
+      if is_some (Context.get_generic_context ()) then
         Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints)
       else ();
   in () end;
@@ -146,7 +146,7 @@
 fun eval (flags: flags) pos toks =
   let
     val space = ML_Env.make_name_space {SML = #SML_env flags, exchange = #exchange flags};
-    val opt_context = Context.thread_data ();
+    val opt_context = Context.get_generic_context ();
 
 
     (* input *)
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/ML/ml_context.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -36,7 +36,8 @@
 fun thms name = Proof_Context.get_thms (Context.the_local_context ()) name;
 
 fun exec (e: unit -> unit) context =
-  (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
+  (case Context.setmp_generic_context (SOME context)
+      (fn () => (e (); Context.get_generic_context ())) () of
     SOME context' => context'
   | NONE => error "Missing context after execution");
 
@@ -170,7 +171,7 @@
     val non_verbose = ML_Compiler.verbose false flags;
 
     (*prepare source text*)
-    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
+    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.get_generic_context ());
     val _ =
       (case env_ctxt of
         SOME ctxt =>
@@ -181,9 +182,10 @@
 
     (*prepare environment*)
     val _ =
-      Context.setmp_thread_data
+      Context.setmp_generic_context
         (Option.map (Context.Proof o Context_Position.set_visible false) env_ctxt)
-        (fn () => (ML_Compiler.eval non_verbose Position.none env; Context.thread_data ())) ()
+        (fn () =>
+          (ML_Compiler.eval non_verbose Position.none env; Context.get_generic_context ())) ()
       |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
 
     (*eval body*)
@@ -191,7 +193,7 @@
 
     (*clear environment*)
     val _ =
-      (case (env_ctxt, is_some (Context.thread_data ())) of
+      (case (env_ctxt, is_some (Context.get_generic_context ())) of
         (SOME ctxt, true) =>
           let
             val name = struct_name ctxt;
@@ -214,17 +216,17 @@
   eval flags (Input.pos_of source) (ML_Lex.read_source (#SML_syntax flags) source);
 
 fun eval_in ctxt flags pos ants =
-  Context.setmp_thread_data (Option.map Context.Proof ctxt)
+  Context.setmp_generic_context (Option.map Context.Proof ctxt)
     (fn () => eval flags pos ants) ();
 
 fun eval_source_in ctxt flags source =
-  Context.setmp_thread_data (Option.map Context.Proof ctxt)
+  Context.setmp_generic_context (Option.map Context.Proof ctxt)
     (fn () => eval_source flags source) ();
 
 fun expression range name constraint body ants =
   exec (fn () =>
     eval ML_Compiler.flags (#1 range)
-     (ML_Lex.read "Context.set_thread_data (SOME (let val " @ ML_Lex.read_set_range range name @
+     (ML_Lex.read "Context.put_generic_context (SOME (let val " @ ML_Lex.read_set_range range name @
       ML_Lex.read (": " ^ constraint ^ " =") @ ants @
       ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));
 
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/ML/ml_env.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -133,7 +133,7 @@
         Context.the_generic_context ()
         |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
       else
-        Context.thread_data ()
+        Context.get_generic_context ()
         |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
         |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
 
@@ -142,7 +142,7 @@
         Context.the_generic_context ()
         |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
       else
-        Context.thread_data ()
+        Context.get_generic_context ()
         |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
         |> append (sel2 ML_Name_Space.global ()))
       |> sort_distinct (string_ord o apply2 #1);
@@ -152,7 +152,7 @@
         Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
           let val sml_tables' = ap1 (Symtab.update entry) sml_tables
           in make_data (bootstrap, tables, sml_tables', breakpoints) end))
-      else if is_some (Context.thread_data ()) then
+      else if is_some (Context.get_generic_context ()) then
         Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
           let
             val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/ML/ml_pervasive1.ML
--- a/src/Pure/ML/ml_pervasive1.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/ML/ml_pervasive1.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -11,4 +11,4 @@
 
 Proofterm.proofs := 0;
 
-Context.set_thread_data NONE;
+Context.put_generic_context NONE;
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/ML/ml_print_depth.ML
--- a/src/Pure/ML/ml_print_depth.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/ML/ml_print_depth.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -25,12 +25,12 @@
 val print_depth = Config.int print_depth_raw;
 
 fun get_print_depth () =
-  (case Context.thread_data () of
+  (case Context.get_generic_context () of
     NONE => ML_Print_Depth.get_print_depth ()
   | SOME context => Config.get_generic context print_depth);
 
 fun get_print_depth_default default =
-  (case Context.thread_data () of
+  (case Context.get_generic_context () of
     NONE => default
   | SOME context => Config.get_generic context print_depth);
 
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/ROOT.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -12,6 +12,7 @@
 use "General/exn.ML";
 
 use "Concurrent/multithreading.ML";
+use "Concurrent/thread_data.ML";
 use "Concurrent/unsynchronized.ML";
 
 use "ML/ml_heap.ML";
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -194,7 +194,7 @@
     val _ = Output.physical_stderr Symbol.STX;
 
     val _ = Printer.show_markup_default := true;
-    val _ = Context.set_thread_data NONE;
+    val _ = Context.put_generic_context NONE;
     val _ =
       Unsynchronized.change print_mode
         (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/Tools/debugger.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -83,17 +83,13 @@
 
 (* stack frame during debugging *)
 
-local
-  val tag = Universal.tag () : ML_Debugger.state list Universal.tag;
-in
+val debugging_var = Thread_Data.var () : ML_Debugger.state list Thread_Data.var;
 
-fun get_debugging () = the_default [] (Thread.getLocal tag);
+fun get_debugging () = the_default [] (Thread_Data.get debugging_var);
 val is_debugging = not o null o get_debugging;
 
 fun with_debugging e =
-  setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e ();
-
-end;
+  Thread_Data.setmp debugging_var (SOME (ML_Debugger.state (Thread.self ()))) e ();
 
 fun the_debug_state thread_name index =
   (case get_debugging () of
@@ -109,14 +105,10 @@
 
 datatype stepping = Stepping of bool * int;  (*stepping enabled, stack depth limit*)
 
-local
-  val tag = Universal.tag () : stepping Universal.tag;
-in
+val stepping_var = Thread_Data.var () : stepping Thread_Data.var;
 
-fun get_stepping () = the_default (Stepping (false, ~1)) (Thread.getLocal tag);
-fun put_stepping stepping = Thread.setLocal (tag, Stepping stepping);
-
-end;
+fun get_stepping () = the_default (Stepping (false, ~1)) (Thread_Data.get stepping_var);
+fun put_stepping stepping = Thread_Data.put stepping_var (SOME (Stepping stepping));
 
 fun is_stepping () =
   let
@@ -137,9 +129,9 @@
 
 val context_attempts =
   map ML_Lex.read
-   ["Context.set_thread_data (SOME (Context.Theory ML_context))",
-    "Context.set_thread_data (SOME (Context.Proof ML_context))",
-    "Context.set_thread_data (SOME ML_context)"];
+   ["Context.put_generic_context (SOME (Context.Theory ML_context))",
+    "Context.put_generic_context (SOME (Context.Proof ML_context))",
+    "Context.put_generic_context (SOME ML_context)"];
 
 fun evaluate {SML, verbose} =
   ML_Context.eval
@@ -180,7 +172,7 @@
   let
     val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
     val context = eval_context thread_name index SML toks1;
-  in Context.setmp_thread_data (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
+  in Context.setmp_generic_context (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
 
 fun print_vals thread_name index SML txt =
   let
@@ -195,7 +187,7 @@
       #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
       |> sort_by #1 |> map (Pretty.item o single o print o #2)
       |> Pretty.chunks |> Pretty.string_of |> writeln_message;
-  in Context.setmp_thread_data (SOME context) print_all () end;
+  in Context.setmp_generic_context (SOME context) print_all () end;
 
 end;
 
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/context.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -73,9 +73,9 @@
   val theory_of: generic -> theory  (*total*)
   val proof_of: generic -> Proof.context  (*total*)
   (*thread data*)
-  val thread_data: unit -> generic option
-  val set_thread_data: generic option -> unit
-  val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
+  val get_generic_context: unit -> generic option
+  val put_generic_context: generic option -> unit
+  val setmp_generic_context: generic option -> ('a -> 'b) -> 'a -> 'b
   val the_generic_context: unit -> generic
   val the_global_context: unit -> theory
   val the_local_context: unit -> Proof.context
@@ -491,18 +491,14 @@
 
 (** thread data **)
 
-local val tag = Universal.tag () : generic option Universal.tag in
+local val generic_context_var = Thread_Data.var () : generic Thread_Data.var in
 
-fun thread_data () =
-  (case Thread.getLocal tag of
-    SOME (SOME context) => SOME context
-  | _ => NONE);
-
-fun set_thread_data context = Thread.setLocal (tag, context);
-fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
+fun get_generic_context () = Thread_Data.get generic_context_var;
+val put_generic_context = Thread_Data.put generic_context_var;
+fun setmp_generic_context opt_context = Thread_Data.setmp generic_context_var opt_context;
 
 fun the_generic_context () =
-  (case thread_data () of
+  (case get_generic_context () of
     SOME context => context
   | _ => error "Unknown context");
 
@@ -514,13 +510,13 @@
 fun >>> f =
   let
     val (res, context') = f (the_generic_context ());
-    val _ = set_thread_data (SOME context');
+    val _ = put_generic_context (SOME context');
   in res end;
 
 nonfix >>;
 fun >> f = >>> (fn context => ((), f context));
 
-val _ = set_thread_data (SOME (Theory pre_pure_thy));
+val _ = put_generic_context (SOME (Theory pre_pure_thy));
 
 end;
 
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/library.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -48,7 +48,6 @@
   val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
   val exists: ('a -> bool) -> 'a list -> bool
   val forall: ('a -> bool) -> 'a list -> bool
-  val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
 
   (*lists*)
   val single: 'a -> 'a list
@@ -278,17 +277,6 @@
 val forall = List.all;
 
 
-(* thread data *)
-
-fun setmp_thread_data tag orig_data data f x =
-  uninterruptible (fn restore_attributes => fn () =>
-    let
-      val _ = Thread.setLocal (tag, data);
-      val result = Exn.capture (restore_attributes f) x;
-      val _ = Thread.setLocal (tag, orig_data);
-    in Exn.release result end) ();
-
-
 
 (** lists **)
 
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -86,9 +86,9 @@
 
 fun value ctxt (get, put, put_ml) (prelude, value) =
   let
-    val code = (prelude
-      ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
-      ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))");
+    val code =
+      prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^
+      put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))";
     val ctxt' = ctxt
       |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
       |> Context.proof_map (exec ctxt false code);
@@ -534,7 +534,7 @@
 fun use_file filepath thy =
   let
     val thy' = Loaded_Values.put [] thy;
-    val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
+    val _ = Context.put_generic_context ((SOME o Context.Theory) thy');
     val _ =
       ML_Compiler0.use_text notifying_context
         {line = 0, file = Path.implode filepath, verbose = false, debug = false}
diff -r 64f44d7279e5 -r 99c7f31615c2 src/Tools/Spec_Check/spec_check.ML
--- a/src/Tools/Spec_Check/spec_check.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Tools/Spec_Check/spec_check.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -134,7 +134,7 @@
       print = fn r => return := r,
       error = #error ML_Env.context}
     val _ =
-      Context.setmp_thread_data (SOME (Context.Proof ctxt))
+      Context.setmp_generic_context (SOME (Context.Proof ctxt))
         (fn () =>
           ML_Compiler0.use_text context
             {line = 0, file = "generated code", verbose = true, debug = false} s) ()
@@ -144,7 +144,7 @@
 
 (*call the compiler and run the test*)
 fun run_test ctxt s =
-  Context.setmp_thread_data (SOME (Context.Proof ctxt))
+  Context.setmp_generic_context (SOME (Context.Proof ctxt))
     (fn () =>
       ML_Compiler0.use_text ML_Env.context
         {line = 0, file = "generated code", verbose = false, debug = false} s) ();