adapted to Context.thread_data interface;
authorwenzelm
Wed Mar 26 22:40:07 2008 +0100 (2008-03-26)
changeset 264151b624d6e9163
parent 26414 2780de5a1422
child 26416 a66f86ef7bb9
adapted to Context.thread_data interface;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof_display.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 26 22:40:05 2008 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 26 22:40:07 2008 +0100
     1.3 @@ -200,7 +200,7 @@
     1.4      \  val oracle: theory -> T -> term = " ^ oracle ^ ";\n\
     1.5      \  val name = " ^ quote name ^ ";\n\
     1.6      \  exception Arg of T;\n\
     1.7 -    \  val _ = ML_Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\
     1.8 +    \  val _ = Context.>> (Theory.add_oracle (name, fn (thy, Arg x) => oracle thy x));\n\
     1.9      \  val thy = ML_Context.the_context ();\n\
    1.10      \  val invoke_" ^ name ^ " = Thm.invoke_oracle_i thy (Sign.full_name thy name);\n\
    1.11      \in\n\
    1.12 @@ -316,7 +316,7 @@
    1.13  val welcome = Toplevel.imperative (writeln o Session.welcome);
    1.14  
    1.15  val exit = Toplevel.keep (fn state =>
    1.16 - (CRITICAL (fn () => ML_Context.set_context (try Toplevel.generic_theory_of state));
    1.17 + (CRITICAL (fn () => Context.set_thread_data (try Toplevel.generic_theory_of state));
    1.18    raise Toplevel.TERMINATE));
    1.19  
    1.20  val quit = Toplevel.imperative quit;
    1.21 @@ -380,7 +380,7 @@
    1.22  (* use ML text *)
    1.23  
    1.24  fun use path = Toplevel.keep (fn state =>
    1.25 -  ML_Context.setmp (try Toplevel.generic_theory_of state) (ThyInfo.load_file false) path);
    1.26 +  Context.setmp_thread_data (try Toplevel.generic_theory_of state) (ThyInfo.load_file false) path);
    1.27  
    1.28  (*passes changes of theory context*)
    1.29  fun use_mltext_theory (txt, pos) =
    1.30 @@ -633,8 +633,8 @@
    1.31  local
    1.32  
    1.33  fun present _ txt true node = OuterSyntax.check_text txt (SOME node)
    1.34 -  | present f (s, _) false node =
    1.35 -      ML_Context.setmp (try (Toplevel.cases_node I (Context.Proof o Proof.context_of)) node) f s;
    1.36 +  | present f (s, _) false node = Context.setmp_thread_data
    1.37 +      (try (Toplevel.cases_node I (Context.Proof o Proof.context_of)) node) f s;
    1.38  
    1.39  fun present_local_theory f (loc, txt) = Toplevel.present_local_theory loc (present f txt);
    1.40  fun present_proof f txt = Toplevel.print o Toplevel.present_proof (present f txt);
     2.1 --- a/src/Pure/Isar/method.ML	Wed Mar 26 22:40:05 2008 +0100
     2.2 +++ b/src/Pure/Isar/method.ML	Wed Mar 26 22:40:07 2008 +0100
     2.3 @@ -357,7 +357,7 @@
     2.4    (ML_Context.use_mltext false pos
     2.5      ("let fun tactic (ctxt: Proof.context) (facts: thm list) : tactic =\n"
     2.6        ^ txt ^ "\nin Method.set_tactic tactic end") (SOME (Context.Proof ctxt));
     2.7 -    ML_Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt)));
     2.8 +    Context.setmp_thread_data (SOME (Context.Proof ctxt)) (! tactic_ref ctxt)));
     2.9  
    2.10  fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
    2.11  fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt);
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Mar 26 22:40:05 2008 +0100
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Mar 26 22:40:07 2008 +0100
     3.3 @@ -309,7 +309,7 @@
     3.4  (* main loop *)
     3.5  
     3.6  fun gen_loop secure do_terminate =
     3.7 - (CRITICAL (fn () => ML_Context.set_context NONE);
     3.8 + (CRITICAL (fn () => Context.set_thread_data NONE);
     3.9    Toplevel.loop secure (isar do_terminate));
    3.10  
    3.11  fun gen_main secure do_terminate =
     4.1 --- a/src/Pure/Isar/proof_display.ML	Wed Mar 26 22:40:05 2008 +0100
     4.2 +++ b/src/Pure/Isar/proof_display.ML	Wed Mar 26 22:40:07 2008 +0100
     4.3 @@ -123,7 +123,7 @@
     4.4  fun present_results ctxt ((kind, name), res) =
     4.5    if kind = "" orelse kind = Thm.internalK then ()
     4.6    else (print_results true ctxt ((kind, name), res);
     4.7 -    ML_Context.setmp (SOME (Context.Proof ctxt))
     4.8 +    Context.setmp_thread_data (SOME (Context.Proof ctxt))
     4.9        (Present.results kind) (name_results name res));
    4.10  
    4.11  end;
     5.1 --- a/src/Pure/Thy/thy_info.ML	Wed Mar 26 22:40:05 2008 +0100
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Mar 26 22:40:07 2008 +0100
     5.3 @@ -278,7 +278,7 @@
     5.4    | provide _ _ _ NONE = NONE;
     5.5  
     5.6  fun run_file path =
     5.7 -  (case Option.map (Context.theory_name o Context.the_theory) (ML_Context.get_context ()) of
     5.8 +  (case Option.map (Context.theory_name o Context.the_theory) (Context.thread_data ()) of
     5.9      NONE => (ThyLoad.load_ml Path.current path; ())
    5.10    | SOME name =>
    5.11        (case lookup_deps name of