src/Pure/ML/ml_context.ML
changeset 62889 99c7f31615c2
parent 62878 1cec457e0a03
child 62900 c641bf9402fd
     1.1 --- a/src/Pure/ML/ml_context.ML	Wed Apr 06 14:08:57 2016 +0200
     1.2 +++ b/src/Pure/ML/ml_context.ML	Wed Apr 06 16:33:33 2016 +0200
     1.3 @@ -36,7 +36,8 @@
     1.4  fun thms name = Proof_Context.get_thms (Context.the_local_context ()) name;
     1.5  
     1.6  fun exec (e: unit -> unit) context =
     1.7 -  (case Context.setmp_thread_data (SOME context) (fn () => (e (); Context.thread_data ())) () of
     1.8 +  (case Context.setmp_generic_context (SOME context)
     1.9 +      (fn () => (e (); Context.get_generic_context ())) () of
    1.10      SOME context' => context'
    1.11    | NONE => error "Missing context after execution");
    1.12  
    1.13 @@ -170,7 +171,7 @@
    1.14      val non_verbose = ML_Compiler.verbose false flags;
    1.15  
    1.16      (*prepare source text*)
    1.17 -    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
    1.18 +    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.get_generic_context ());
    1.19      val _ =
    1.20        (case env_ctxt of
    1.21          SOME ctxt =>
    1.22 @@ -181,9 +182,10 @@
    1.23  
    1.24      (*prepare environment*)
    1.25      val _ =
    1.26 -      Context.setmp_thread_data
    1.27 +      Context.setmp_generic_context
    1.28          (Option.map (Context.Proof o Context_Position.set_visible false) env_ctxt)
    1.29 -        (fn () => (ML_Compiler.eval non_verbose Position.none env; Context.thread_data ())) ()
    1.30 +        (fn () =>
    1.31 +          (ML_Compiler.eval non_verbose Position.none env; Context.get_generic_context ())) ()
    1.32        |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
    1.33  
    1.34      (*eval body*)
    1.35 @@ -191,7 +193,7 @@
    1.36  
    1.37      (*clear environment*)
    1.38      val _ =
    1.39 -      (case (env_ctxt, is_some (Context.thread_data ())) of
    1.40 +      (case (env_ctxt, is_some (Context.get_generic_context ())) of
    1.41          (SOME ctxt, true) =>
    1.42            let
    1.43              val name = struct_name ctxt;
    1.44 @@ -214,17 +216,17 @@
    1.45    eval flags (Input.pos_of source) (ML_Lex.read_source (#SML_syntax flags) source);
    1.46  
    1.47  fun eval_in ctxt flags pos ants =
    1.48 -  Context.setmp_thread_data (Option.map Context.Proof ctxt)
    1.49 +  Context.setmp_generic_context (Option.map Context.Proof ctxt)
    1.50      (fn () => eval flags pos ants) ();
    1.51  
    1.52  fun eval_source_in ctxt flags source =
    1.53 -  Context.setmp_thread_data (Option.map Context.Proof ctxt)
    1.54 +  Context.setmp_generic_context (Option.map Context.Proof ctxt)
    1.55      (fn () => eval_source flags source) ();
    1.56  
    1.57  fun expression range name constraint body ants =
    1.58    exec (fn () =>
    1.59      eval ML_Compiler.flags (#1 range)
    1.60 -     (ML_Lex.read "Context.set_thread_data (SOME (let val " @ ML_Lex.read_set_range range name @
    1.61 +     (ML_Lex.read "Context.put_generic_context (SOME (let val " @ ML_Lex.read_set_range range name @
    1.62        ML_Lex.read (": " ^ constraint ^ " =") @ ants @
    1.63        ML_Lex.read ("in " ^ body ^ " end (Context.the_generic_context ())));")));
    1.64