clarified modules;
authorwenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 6288999c7f31615c2
parent 62888 64f44d7279e5
child 62890 728aa05e9433
clarified modules;
tuned signature;
src/HOL/Tools/Quickcheck/narrowing_generators.ML
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/standard_thread.ML
src/Pure/Concurrent/thread_data.ML
src/Pure/General/position.ML
src/Pure/General/print_mode.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/runtime.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML/exn_debugger.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_pervasive1.ML
src/Pure/ML/ml_print_depth.ML
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.ML
src/Pure/Tools/debugger.ML
src/Pure/context.ML
src/Pure/library.ML
src/Tools/Code/code_runtime.ML
src/Tools/Spec_Check/spec_check.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 06 14:08:57 2016 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 06 16:33:33 2016 +0200
     1.3 @@ -279,7 +279,8 @@
     1.4                  let
     1.5                    val output_value = the_default "NONE"
     1.6                      (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
     1.7 -                  val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
     1.8 +                  val ml_code =
     1.9 +                    "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^ put_ml
    1.10                      ^ " (fn () => " ^ output_value ^ ")) (Context.the_generic_context ())))";
    1.11                    val ctxt' = ctxt
    1.12                      |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
     2.1 --- a/src/Pure/Concurrent/future.ML	Wed Apr 06 14:08:57 2016 +0200
     2.2 +++ b/src/Pure/Concurrent/future.ML	Wed Apr 06 16:33:33 2016 +0200
     2.3 @@ -58,10 +58,10 @@
     2.4  (* identifiers *)
     2.5  
     2.6  local
     2.7 -  val tag = Universal.tag () : task option Universal.tag;
     2.8 +  val worker_task_var = Thread_Data.var () : task Thread_Data.var;
     2.9  in
    2.10 -  fun worker_task () = the_default NONE (Thread.getLocal tag);
    2.11 -  fun setmp_worker_task task f x = setmp_thread_data tag (worker_task ()) (SOME task) f x;
    2.12 +  fun worker_task () = Thread_Data.get worker_task_var;
    2.13 +  fun setmp_worker_task task f x = Thread_Data.setmp worker_task_var (SOME task) f x;
    2.14  end;
    2.15  
    2.16  val worker_group = Option.map Task_Queue.group_of_task o worker_task;
    2.17 @@ -432,14 +432,14 @@
    2.18    let
    2.19      val result = Single_Assignment.var "future" : 'a result;
    2.20      val pos = Position.thread_data ();
    2.21 -    val context = Context.thread_data ();
    2.22 +    val context = Context.get_generic_context ();
    2.23      fun job ok =
    2.24        let
    2.25          val res =
    2.26            if ok then
    2.27              Exn.capture (fn () =>
    2.28                Multithreading.with_attributes atts (fn _ =>
    2.29 -                (Position.setmp_thread_data pos o Context.setmp_thread_data context) e ())) ()
    2.30 +                (Position.setmp_thread_data pos o Context.setmp_generic_context context) e ())) ()
    2.31            else Exn.interrupt_exn;
    2.32        in assign_result group result (identify_result pos res) end;
    2.33    in (result, job) end;
     3.1 --- a/src/Pure/Concurrent/standard_thread.ML	Wed Apr 06 14:08:57 2016 +0200
     3.2 +++ b/src/Pure/Concurrent/standard_thread.ML	Wed Apr 06 16:33:33 2016 +0200
     3.3 @@ -27,11 +27,11 @@
     3.4  (* unique name *)
     3.5  
     3.6  local
     3.7 -  val tag = Universal.tag () : string Universal.tag;
     3.8 +  val name_var = Thread_Data.var () : string Thread_Data.var;
     3.9    val count = Counter.make ();
    3.10  in
    3.11  
    3.12 -fun get_name () = Thread.getLocal tag;
    3.13 +fun get_name () = Thread_Data.get name_var;
    3.14  
    3.15  fun the_name () =
    3.16    (case get_name () of
    3.17 @@ -39,7 +39,7 @@
    3.18    | SOME name => name);
    3.19  
    3.20  fun set_name base =
    3.21 -  Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
    3.22 +  Thread_Data.put name_var (SOME (base ^ "/" ^ string_of_int (count ())));
    3.23  
    3.24  end;
    3.25  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Concurrent/thread_data.ML	Wed Apr 06 16:33:33 2016 +0200
     4.3 @@ -0,0 +1,42 @@
     4.4 +(*  Title:      Pure/Concurrent/thread_data.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Thread-local data -- raw version without context management.
     4.8 +*)
     4.9 +
    4.10 +signature THREAD_DATA =
    4.11 +sig
    4.12 +  type 'a var
    4.13 +  val var: unit -> 'a var
    4.14 +  val get: 'a var -> 'a option
    4.15 +  val put: 'a var -> 'a option -> unit
    4.16 +  val setmp: 'a var -> 'a option -> ('b -> 'c) -> 'b -> 'c
    4.17 +end;
    4.18 +
    4.19 +structure Thread_Data: THREAD_DATA =
    4.20 +struct
    4.21 +
    4.22 +abstype 'a var = Var of 'a option Universal.tag
    4.23 +with
    4.24 +
    4.25 +fun var () : 'a var = Var (Universal.tag ());
    4.26 +
    4.27 +fun get (Var tag) =
    4.28 +  (case Thread.getLocal tag of
    4.29 +    SOME data => data
    4.30 +  | NONE => NONE);
    4.31 +
    4.32 +fun put (Var tag) data = Thread.setLocal (tag, data);
    4.33 +
    4.34 +fun setmp v data f x =
    4.35 +  uninterruptible (fn restore_attributes => fn () =>
    4.36 +    let
    4.37 +      val orig_data = get v;
    4.38 +      val _ = put v data;
    4.39 +      val result = Exn.capture (restore_attributes f) x;
    4.40 +      val _ = put v orig_data;
    4.41 +    in Exn.release result end) ();
    4.42 +
    4.43 +end;
    4.44 +
    4.45 +end;
     5.1 --- a/src/Pure/General/position.ML	Wed Apr 06 14:08:57 2016 +0200
     5.2 +++ b/src/Pure/General/position.ML	Wed Apr 06 16:33:33 2016 +0200
     5.3 @@ -243,13 +243,9 @@
     5.4  
     5.5  (* thread data *)
     5.6  
     5.7 -local val tag = Universal.tag () : T Universal.tag in
     5.8 -
     5.9 -fun thread_data () = the_default none (Thread.getLocal tag);
    5.10 -
    5.11 -fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos;
    5.12 -
    5.13 -end;
    5.14 +val thread_data_var = Thread_Data.var () : T Thread_Data.var;
    5.15 +fun thread_data () = the_default none (Thread_Data.get thread_data_var);
    5.16 +fun setmp_thread_data pos = Thread_Data.setmp thread_data_var (SOME pos);
    5.17  
    5.18  fun default pos =
    5.19    if pos = none then (false, thread_data ())
     6.1 --- a/src/Pure/General/print_mode.ML	Wed Apr 06 14:08:57 2016 +0200
     6.2 +++ b/src/Pure/General/print_mode.ML	Wed Apr 06 16:33:33 2016 +0200
     6.3 @@ -34,20 +34,18 @@
     6.4  val internal = "internal";
     6.5  
     6.6  val print_mode = Unsynchronized.ref ([]: string list);
     6.7 -val tag = Universal.tag () : string list option Universal.tag;
     6.8 +val print_mode_var = Thread_Data.var () : string list Thread_Data.var;
     6.9  
    6.10  fun print_mode_value () =
    6.11    let val modes =
    6.12 -    (case Thread.getLocal tag of
    6.13 -      SOME (SOME modes) => modes
    6.14 -    | _ => ! print_mode)
    6.15 +    (case Thread_Data.get print_mode_var of
    6.16 +      SOME modes => modes
    6.17 +    | NONE => ! print_mode)
    6.18    in subtract (op =) [input, internal] modes end;
    6.19  
    6.20  fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
    6.21  
    6.22 -fun setmp modes f x =
    6.23 -  let val orig_modes = (case Thread.getLocal tag of SOME (SOME ms) => SOME ms | _ => NONE)
    6.24 -  in setmp_thread_data tag orig_modes (SOME modes) f x end;
    6.25 +fun setmp modes f x = Thread_Data.setmp print_mode_var (SOME modes) f x;
    6.26  
    6.27  fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
    6.28  fun closure f = with_modes [] f;
     7.1 --- a/src/Pure/Isar/method.ML	Wed Apr 06 14:08:57 2016 +0200
     7.2 +++ b/src/Pure/Isar/method.ML	Wed Apr 06 16:33:33 2016 +0200
     7.3 @@ -355,8 +355,7 @@
     7.4               ML_Lex.read_source false source);
     7.5          val tac = the_tactic context';
     7.6        in
     7.7 -        fn phi =>
     7.8 -          set_tactic (fn _ => Context.setmp_thread_data (SOME context) (tac phi))
     7.9 +        fn phi => set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi))
    7.10        end)) >> (fn decl => Morphism.form (the_tactic (Morphism.form decl context))));
    7.11  
    7.12  
     8.1 --- a/src/Pure/Isar/proof_display.ML	Wed Apr 06 14:08:57 2016 +0200
     8.2 +++ b/src/Pure/Isar/proof_display.ML	Wed Apr 06 16:33:33 2016 +0200
     8.3 @@ -39,7 +39,7 @@
     8.4    else Pretty.str "<context>");
     8.5  
     8.6  fun default_context mk_thy =
     8.7 -  (case Context.thread_data () of
     8.8 +  (case Context.get_generic_context () of
     8.9      SOME (Context.Proof ctxt) => ctxt
    8.10    | SOME (Context.Theory thy) =>
    8.11        (case try Syntax.init_pretty_global thy of
     9.1 --- a/src/Pure/Isar/runtime.ML	Wed Apr 06 14:08:57 2016 +0200
     9.2 +++ b/src/Pure/Isar/runtime.ML	Wed Apr 06 16:33:33 2016 +0200
     9.3 @@ -54,7 +54,7 @@
     9.4    | exn_context (SOME ctxt) exn = if Exn.is_interrupt exn then exn else CONTEXT (ctxt, exn);
     9.5  
     9.6  fun thread_context exn =
     9.7 -  exn_context (Option.map Context.proof_of (Context.thread_data ())) exn;
     9.8 +  exn_context (Option.map Context.proof_of (Context.get_generic_context ())) exn;
     9.9  
    9.10  
    9.11  (* exn_message *)
    9.12 @@ -202,7 +202,7 @@
    9.13      else
    9.14        let
    9.15          val opt_ctxt =
    9.16 -          (case Context.thread_data () of
    9.17 +          (case Context.get_generic_context () of
    9.18              NONE => NONE
    9.19            | SOME context => try Context.proof_of context);
    9.20          val _ = output_exn (exn_context opt_ctxt exn);
    10.1 --- a/src/Pure/Isar/toplevel.ML	Wed Apr 06 14:08:57 2016 +0200
    10.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Apr 06 16:33:33 2016 +0200
    10.3 @@ -574,7 +574,7 @@
    10.4  fun transition int tr st =
    10.5    let
    10.6      val (st', opt_err) =
    10.7 -      Context.setmp_thread_data (try (Context.Proof o presentation_context_of) st)
    10.8 +      Context.setmp_generic_context (try (Context.Proof o presentation_context_of) st)
    10.9          (fn () => app int tr st) ();
   10.10      val opt_err' = opt_err |> Option.map
   10.11        (fn Runtime.EXCURSION_FAIL exn_info => exn_info
    11.1 --- a/src/Pure/ML/exn_debugger.ML	Wed Apr 06 14:08:57 2016 +0200
    11.2 +++ b/src/Pure/ML/exn_debugger.ML	Wed Apr 06 16:33:33 2016 +0200
    11.3 @@ -15,28 +15,24 @@
    11.4  
    11.5  (* thread data *)
    11.6  
    11.7 -local
    11.8 -  val tag =
    11.9 -    Universal.tag () : ((string * ML_Compiler0.polyml_location) * exn) list option Universal.tag;
   11.10 -in
   11.11 +val trace_var =
   11.12 +  Thread_Data.var () : ((string * ML_Compiler0.polyml_location) * exn) list Thread_Data.var;
   11.13  
   11.14 -fun start_trace () = Thread.setLocal (tag, SOME []);
   11.15 +fun start_trace () = Thread_Data.put trace_var (SOME []);
   11.16  
   11.17  fun update_trace entry exn =
   11.18 -  (case Thread.getLocal tag of
   11.19 -    SOME (SOME trace) => Thread.setLocal (tag, SOME ((entry, exn) :: trace))
   11.20 -  | _ => ());
   11.21 +  (case Thread_Data.get trace_var of
   11.22 +    SOME trace => Thread_Data.put trace_var (SOME ((entry, exn) :: trace))
   11.23 +  | NONE => ());
   11.24  
   11.25  fun stop_trace () =
   11.26    let
   11.27 -    val trace = (case Thread.getLocal tag of SOME (SOME trace) => trace | _ => []);
   11.28 -    val _ = Thread.setLocal (tag, NONE);
   11.29 +    val trace = the_default [] (Thread_Data.get trace_var);
   11.30 +    val _ = Thread_Data.put trace_var NONE;
   11.31    in trace end;
   11.32  
   11.33  val _ = ML_Debugger.on_exit_exception (SOME update_trace);
   11.34  
   11.35 -end;
   11.36 -
   11.37  
   11.38  (* capture exception trace *)
   11.39  
    12.1 --- a/src/Pure/ML/ml_compiler.ML	Wed Apr 06 14:08:57 2016 +0200
    12.2 +++ b/src/Pure/ML/ml_compiler.ML	Wed Apr 06 16:33:33 2016 +0200
    12.3 @@ -52,7 +52,7 @@
    12.4  fun report_parse_tree redirect depth space parse_tree =
    12.5    let
    12.6      val is_visible =
    12.7 -      (case Context.thread_data () of
    12.8 +      (case Context.get_generic_context () of
    12.9          SOME context => Context_Position.is_visible_generic context
   12.10        | NONE => true);
   12.11      fun is_reported pos = is_visible andalso Position.is_reported pos;
   12.12 @@ -135,7 +135,7 @@
   12.13      val all_breakpoints = rev (breakpoints_tree parse_tree []);
   12.14      val _ = Position.reports (map #1 all_breakpoints);
   12.15      val _ =
   12.16 -      if is_some (Context.thread_data ()) then
   12.17 +      if is_some (Context.get_generic_context ()) then
   12.18          Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints)
   12.19        else ();
   12.20    in () end;
   12.21 @@ -146,7 +146,7 @@
   12.22  fun eval (flags: flags) pos toks =
   12.23    let
   12.24      val space = ML_Env.make_name_space {SML = #SML_env flags, exchange = #exchange flags};
   12.25 -    val opt_context = Context.thread_data ();
   12.26 +    val opt_context = Context.get_generic_context ();
   12.27  
   12.28  
   12.29      (* input *)
    13.1 --- a/src/Pure/ML/ml_context.ML	Wed Apr 06 14:08:57 2016 +0200
    13.2 +++ b/src/Pure/ML/ml_context.ML	Wed Apr 06 16:33:33 2016 +0200
    13.3 @@ -36,7 +36,8 @@
    13.4  fun thms name = Proof_Context.get_thms (Context.the_local_context ()) name;
    13.5  
    13.6  fun exec (e: unit -> unit) context =
    13.7 -  (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
    13.8 +  (case Context.setmp_generic_context (SOME context)
    13.9 +      (fn () => (e (); Context.get_generic_context ())) () of
   13.10      SOME context' => context'
   13.11    | NONE => error "Missing context after execution");
   13.12  
   13.13 @@ -170,7 +171,7 @@
   13.14      val non_verbose = ML_Compiler.verbose false flags;
   13.15  
   13.16      (*prepare source text*)
   13.17 -    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
   13.18 +    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.get_generic_context ());
   13.19      val _ =
   13.20        (case env_ctxt of
   13.21          SOME ctxt =>
   13.22 @@ -181,9 +182,10 @@
   13.23  
   13.24      (*prepare environment*)
   13.25      val _ =
   13.26 -      Context.setmp_thread_data
   13.27 +      Context.setmp_generic_context
   13.28          (Option.map (Context.Proof o Context_Position.set_visible false) env_ctxt)
   13.29 -        (fn () => (ML_Compiler.eval non_verbose Position.none env; Context.thread_data ())) ()
   13.30 +        (fn () =>
   13.31 +          (ML_Compiler.eval non_verbose Position.none env; Context.get_generic_context ())) ()
   13.32        |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
   13.33  
   13.34      (*eval body*)
   13.35 @@ -191,7 +193,7 @@
   13.36  
   13.37      (*clear environment*)
   13.38      val _ =
   13.39 -      (case (env_ctxt, is_some (Context.thread_data ())) of
   13.40 +      (case (env_ctxt, is_some (Context.get_generic_context ())) of
   13.41          (SOME ctxt, true) =>
   13.42            let
   13.43              val name = struct_name ctxt;
   13.44 @@ -214,17 +216,17 @@
   13.45    eval flags (Input.pos_of source) (ML_Lex.read_source (#SML_syntax flags) source);
   13.46  
   13.47  fun eval_in ctxt flags pos ants =
   13.48 -  Context.setmp_thread_data (Option.map Context.Proof ctxt)
   13.49 +  Context.setmp_generic_context (Option.map Context.Proof ctxt)
   13.50      (fn () => eval flags pos ants) ();
   13.51  
   13.52  fun eval_source_in ctxt flags source =
   13.53 -  Context.setmp_thread_data (Option.map Context.Proof ctxt)
   13.54 +  Context.setmp_generic_context (Option.map Context.Proof ctxt)
   13.55      (fn () => eval_source flags source) ();
   13.56  
   13.57  fun expression range name constraint body ants =
   13.58    exec (fn () =>
   13.59      eval ML_Compiler.flags (#1 range)
   13.60 -     (ML_Lex.read "Context.set_thread_data (SOME (let val " @ ML_Lex.read_set_range range name @
   13.61 +     (ML_Lex.read "Context.put_generic_context (SOME (let val " @ ML_Lex.read_set_range range name @
   13.62        ML_Lex.read (": " ^ constraint ^ " =") @ ants @
   13.63        ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));
   13.64  
    14.1 --- a/src/Pure/ML/ml_env.ML	Wed Apr 06 14:08:57 2016 +0200
    14.2 +++ b/src/Pure/ML/ml_env.ML	Wed Apr 06 16:33:33 2016 +0200
    14.3 @@ -133,7 +133,7 @@
    14.4          Context.the_generic_context ()
    14.5          |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
    14.6        else
    14.7 -        Context.thread_data ()
    14.8 +        Context.get_generic_context ()
    14.9          |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
   14.10          |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
   14.11  
   14.12 @@ -142,7 +142,7 @@
   14.13          Context.the_generic_context ()
   14.14          |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
   14.15        else
   14.16 -        Context.thread_data ()
   14.17 +        Context.get_generic_context ()
   14.18          |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
   14.19          |> append (sel2 ML_Name_Space.global ()))
   14.20        |> sort_distinct (string_ord o apply2 #1);
   14.21 @@ -152,7 +152,7 @@
   14.22          Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
   14.23            let val sml_tables' = ap1 (Symtab.update entry) sml_tables
   14.24            in make_data (bootstrap, tables, sml_tables', breakpoints) end))
   14.25 -      else if is_some (Context.thread_data ()) then
   14.26 +      else if is_some (Context.get_generic_context ()) then
   14.27          Context.>> (Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
   14.28            let
   14.29              val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
    15.1 --- a/src/Pure/ML/ml_pervasive1.ML	Wed Apr 06 14:08:57 2016 +0200
    15.2 +++ b/src/Pure/ML/ml_pervasive1.ML	Wed Apr 06 16:33:33 2016 +0200
    15.3 @@ -11,4 +11,4 @@
    15.4  
    15.5  Proofterm.proofs := 0;
    15.6  
    15.7 -Context.set_thread_data NONE;
    15.8 +Context.put_generic_context NONE;
    16.1 --- a/src/Pure/ML/ml_print_depth.ML	Wed Apr 06 14:08:57 2016 +0200
    16.2 +++ b/src/Pure/ML/ml_print_depth.ML	Wed Apr 06 16:33:33 2016 +0200
    16.3 @@ -25,12 +25,12 @@
    16.4  val print_depth = Config.int print_depth_raw;
    16.5  
    16.6  fun get_print_depth () =
    16.7 -  (case Context.thread_data () of
    16.8 +  (case Context.get_generic_context () of
    16.9      NONE => ML_Print_Depth.get_print_depth ()
   16.10    | SOME context => Config.get_generic context print_depth);
   16.11  
   16.12  fun get_print_depth_default default =
   16.13 -  (case Context.thread_data () of
   16.14 +  (case Context.get_generic_context () of
   16.15      NONE => default
   16.16    | SOME context => Config.get_generic context print_depth);
   16.17  
    17.1 --- a/src/Pure/ROOT.ML	Wed Apr 06 14:08:57 2016 +0200
    17.2 +++ b/src/Pure/ROOT.ML	Wed Apr 06 16:33:33 2016 +0200
    17.3 @@ -12,6 +12,7 @@
    17.4  use "General/exn.ML";
    17.5  
    17.6  use "Concurrent/multithreading.ML";
    17.7 +use "Concurrent/thread_data.ML";
    17.8  use "Concurrent/unsynchronized.ML";
    17.9  
   17.10  use "ML/ml_heap.ML";
    18.1 --- a/src/Pure/System/isabelle_process.ML	Wed Apr 06 14:08:57 2016 +0200
    18.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Apr 06 16:33:33 2016 +0200
    18.3 @@ -194,7 +194,7 @@
    18.4      val _ = Output.physical_stderr Symbol.STX;
    18.5  
    18.6      val _ = Printer.show_markup_default := true;
    18.7 -    val _ = Context.set_thread_data NONE;
    18.8 +    val _ = Context.put_generic_context NONE;
    18.9      val _ =
   18.10        Unsynchronized.change print_mode
   18.11          (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
    19.1 --- a/src/Pure/Tools/debugger.ML	Wed Apr 06 14:08:57 2016 +0200
    19.2 +++ b/src/Pure/Tools/debugger.ML	Wed Apr 06 16:33:33 2016 +0200
    19.3 @@ -83,17 +83,13 @@
    19.4  
    19.5  (* stack frame during debugging *)
    19.6  
    19.7 -local
    19.8 -  val tag = Universal.tag () : ML_Debugger.state list Universal.tag;
    19.9 -in
   19.10 +val debugging_var = Thread_Data.var () : ML_Debugger.state list Thread_Data.var;
   19.11  
   19.12 -fun get_debugging () = the_default [] (Thread.getLocal tag);
   19.13 +fun get_debugging () = the_default [] (Thread_Data.get debugging_var);
   19.14  val is_debugging = not o null o get_debugging;
   19.15  
   19.16  fun with_debugging e =
   19.17 -  setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e ();
   19.18 -
   19.19 -end;
   19.20 +  Thread_Data.setmp debugging_var (SOME (ML_Debugger.state (Thread.self ()))) e ();
   19.21  
   19.22  fun the_debug_state thread_name index =
   19.23    (case get_debugging () of
   19.24 @@ -109,14 +105,10 @@
   19.25  
   19.26  datatype stepping = Stepping of bool * int;  (*stepping enabled, stack depth limit*)
   19.27  
   19.28 -local
   19.29 -  val tag = Universal.tag () : stepping Universal.tag;
   19.30 -in
   19.31 +val stepping_var = Thread_Data.var () : stepping Thread_Data.var;
   19.32  
   19.33 -fun get_stepping () = the_default (Stepping (false, ~1)) (Thread.getLocal tag);
   19.34 -fun put_stepping stepping = Thread.setLocal (tag, Stepping stepping);
   19.35 -
   19.36 -end;
   19.37 +fun get_stepping () = the_default (Stepping (false, ~1)) (Thread_Data.get stepping_var);
   19.38 +fun put_stepping stepping = Thread_Data.put stepping_var (SOME (Stepping stepping));
   19.39  
   19.40  fun is_stepping () =
   19.41    let
   19.42 @@ -137,9 +129,9 @@
   19.43  
   19.44  val context_attempts =
   19.45    map ML_Lex.read
   19.46 -   ["Context.set_thread_data (SOME (Context.Theory ML_context))",
   19.47 -    "Context.set_thread_data (SOME (Context.Proof ML_context))",
   19.48 -    "Context.set_thread_data (SOME ML_context)"];
   19.49 +   ["Context.put_generic_context (SOME (Context.Theory ML_context))",
   19.50 +    "Context.put_generic_context (SOME (Context.Proof ML_context))",
   19.51 +    "Context.put_generic_context (SOME ML_context)"];
   19.52  
   19.53  fun evaluate {SML, verbose} =
   19.54    ML_Context.eval
   19.55 @@ -180,7 +172,7 @@
   19.56    let
   19.57      val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
   19.58      val context = eval_context thread_name index SML toks1;
   19.59 -  in Context.setmp_thread_data (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
   19.60 +  in Context.setmp_generic_context (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
   19.61  
   19.62  fun print_vals thread_name index SML txt =
   19.63    let
   19.64 @@ -195,7 +187,7 @@
   19.65        #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
   19.66        |> sort_by #1 |> map (Pretty.item o single o print o #2)
   19.67        |> Pretty.chunks |> Pretty.string_of |> writeln_message;
   19.68 -  in Context.setmp_thread_data (SOME context) print_all () end;
   19.69 +  in Context.setmp_generic_context (SOME context) print_all () end;
   19.70  
   19.71  end;
   19.72  
    20.1 --- a/src/Pure/context.ML	Wed Apr 06 14:08:57 2016 +0200
    20.2 +++ b/src/Pure/context.ML	Wed Apr 06 16:33:33 2016 +0200
    20.3 @@ -73,9 +73,9 @@
    20.4    val theory_of: generic -> theory  (*total*)
    20.5    val proof_of: generic -> Proof.context  (*total*)
    20.6    (*thread data*)
    20.7 -  val thread_data: unit -> generic option
    20.8 -  val set_thread_data: generic option -> unit
    20.9 -  val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
   20.10 +  val get_generic_context: unit -> generic option
   20.11 +  val put_generic_context: generic option -> unit
   20.12 +  val setmp_generic_context: generic option -> ('a -> 'b) -> 'a -> 'b
   20.13    val the_generic_context: unit -> generic
   20.14    val the_global_context: unit -> theory
   20.15    val the_local_context: unit -> Proof.context
   20.16 @@ -491,18 +491,14 @@
   20.17  
   20.18  (** thread data **)
   20.19  
   20.20 -local val tag = Universal.tag () : generic option Universal.tag in
   20.21 +local val generic_context_var = Thread_Data.var () : generic Thread_Data.var in
   20.22  
   20.23 -fun thread_data () =
   20.24 -  (case Thread.getLocal tag of
   20.25 -    SOME (SOME context) => SOME context
   20.26 -  | _ => NONE);
   20.27 -
   20.28 -fun set_thread_data context = Thread.setLocal (tag, context);
   20.29 -fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
   20.30 +fun get_generic_context () = Thread_Data.get generic_context_var;
   20.31 +val put_generic_context = Thread_Data.put generic_context_var;
   20.32 +fun setmp_generic_context opt_context = Thread_Data.setmp generic_context_var opt_context;
   20.33  
   20.34  fun the_generic_context () =
   20.35 -  (case thread_data () of
   20.36 +  (case get_generic_context () of
   20.37      SOME context => context
   20.38    | _ => error "Unknown context");
   20.39  
   20.40 @@ -514,13 +510,13 @@
   20.41  fun >>> f =
   20.42    let
   20.43      val (res, context') = f (the_generic_context ());
   20.44 -    val _ = set_thread_data (SOME context');
   20.45 +    val _ = put_generic_context (SOME context');
   20.46    in res end;
   20.47  
   20.48  nonfix >>;
   20.49  fun >> f = >>> (fn context => ((), f context));
   20.50  
   20.51 -val _ = set_thread_data (SOME (Theory pre_pure_thy));
   20.52 +val _ = put_generic_context (SOME (Theory pre_pure_thy));
   20.53  
   20.54  end;
   20.55  
    21.1 --- a/src/Pure/library.ML	Wed Apr 06 14:08:57 2016 +0200
    21.2 +++ b/src/Pure/library.ML	Wed Apr 06 16:33:33 2016 +0200
    21.3 @@ -48,7 +48,6 @@
    21.4    val andf: ('a -> bool) * ('a -> bool) -> 'a -> bool
    21.5    val exists: ('a -> bool) -> 'a list -> bool
    21.6    val forall: ('a -> bool) -> 'a list -> bool
    21.7 -  val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
    21.8  
    21.9    (*lists*)
   21.10    val single: 'a -> 'a list
   21.11 @@ -278,17 +277,6 @@
   21.12  val forall = List.all;
   21.13  
   21.14  
   21.15 -(* thread data *)
   21.16 -
   21.17 -fun setmp_thread_data tag orig_data data f x =
   21.18 -  uninterruptible (fn restore_attributes => fn () =>
   21.19 -    let
   21.20 -      val _ = Thread.setLocal (tag, data);
   21.21 -      val result = Exn.capture (restore_attributes f) x;
   21.22 -      val _ = Thread.setLocal (tag, orig_data);
   21.23 -    in Exn.release result end) ();
   21.24 -
   21.25 -
   21.26  
   21.27  (** lists **)
   21.28  
    22.1 --- a/src/Tools/Code/code_runtime.ML	Wed Apr 06 14:08:57 2016 +0200
    22.2 +++ b/src/Tools/Code/code_runtime.ML	Wed Apr 06 16:33:33 2016 +0200
    22.3 @@ -86,9 +86,9 @@
    22.4  
    22.5  fun value ctxt (get, put, put_ml) (prelude, value) =
    22.6    let
    22.7 -    val code = (prelude
    22.8 -      ^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
    22.9 -      ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))");
   22.10 +    val code =
   22.11 +      prelude ^ "\nval _ = Context.put_generic_context (SOME (Context.map_proof (" ^
   22.12 +      put_ml ^ " (fn () => " ^ value ^ ")) (Context.the_generic_context ())))";
   22.13      val ctxt' = ctxt
   22.14        |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
   22.15        |> Context.proof_map (exec ctxt false code);
   22.16 @@ -534,7 +534,7 @@
   22.17  fun use_file filepath thy =
   22.18    let
   22.19      val thy' = Loaded_Values.put [] thy;
   22.20 -    val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
   22.21 +    val _ = Context.put_generic_context ((SOME o Context.Theory) thy');
   22.22      val _ =
   22.23        ML_Compiler0.use_text notifying_context
   22.24          {line = 0, file = Path.implode filepath, verbose = false, debug = false}
    23.1 --- a/src/Tools/Spec_Check/spec_check.ML	Wed Apr 06 14:08:57 2016 +0200
    23.2 +++ b/src/Tools/Spec_Check/spec_check.ML	Wed Apr 06 16:33:33 2016 +0200
    23.3 @@ -134,7 +134,7 @@
    23.4        print = fn r => return := r,
    23.5        error = #error ML_Env.context}
    23.6      val _ =
    23.7 -      Context.setmp_thread_data (SOME (Context.Proof ctxt))
    23.8 +      Context.setmp_generic_context (SOME (Context.Proof ctxt))
    23.9          (fn () =>
   23.10            ML_Compiler0.use_text context
   23.11              {line = 0, file = "generated code", verbose = true, debug = false} s) ()
   23.12 @@ -144,7 +144,7 @@
   23.13  
   23.14  (*call the compiler and run the test*)
   23.15  fun run_test ctxt s =
   23.16 -  Context.setmp_thread_data (SOME (Context.Proof ctxt))
   23.17 +  Context.setmp_generic_context (SOME (Context.Proof ctxt))
   23.18      (fn () =>
   23.19        ML_Compiler0.use_text ML_Env.context
   23.20          {line = 0, file = "generated code", verbose = false, debug = false} s) ();