# 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 ""); 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) ();