adapted ML context operations;
authorwenzelm
Fri Jan 19 13:09:33 2007 +0100 (2007-01-19)
changeset 22086cf6019fece63
parent 22085 c138cfd500f7
child 22087 a13299166175
adapted ML context operations;
src/Pure/Isar/isar_output.ML
src/Pure/Isar/method.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof_display.ML
src/Pure/Thy/thm_database.ML
src/Pure/Thy/thy_info.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/Isar/isar_output.ML	Fri Jan 19 13:09:32 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_output.ML	Fri Jan 19 13:09:33 2007 +0100
     1.3 @@ -509,7 +509,7 @@
     1.4  fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
     1.5  
     1.6  fun output_ml ml src ctxt txt =
     1.7 - (Context.use_mltext (ml txt) false (SOME (ProofContext.theory_of ctxt));
     1.8 + (Context.use_mltext (ml txt) false (SOME (Context.Proof ctxt));
     1.9    (if ! source then str_of_source src else txt)
    1.10    |> (if ! quotes then quote else I)
    1.11    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
     2.1 --- a/src/Pure/Isar/method.ML	Fri Jan 19 13:09:32 2007 +0100
     2.2 +++ b/src/Pure/Isar/method.ML	Fri Jan 19 13:09:33 2007 +0100
     2.3 @@ -348,7 +348,7 @@
     2.4         ^ txt ^
     2.5         "\nend in Method.set_tactic tactic end")
     2.6      false NONE;
     2.7 -    Context.setmp (SOME (ProofContext.theory_of ctxt)) (! tactic_ref ctxt) facts));
     2.8 +    Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts));
     2.9  
    2.10  
    2.11  
    2.12 @@ -448,8 +448,9 @@
    2.13      "val thm = PureThy.get_thm_closure (Context.the_context ()) o PureThy.Name;\n\
    2.14      \val thms = PureThy.get_thms_closure (Context.the_context ()) o PureThy.Name;\n\
    2.15      \val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
    2.16 -    "Method.add_method method"
    2.17 -    ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
    2.18 +    "Context.map_theory (Method.add_method method)"
    2.19 +    ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")")
    2.20 +  |> Context.theory_map;
    2.21  
    2.22  
    2.23  
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Jan 19 13:09:32 2007 +0100
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Jan 19 13:09:33 2007 +0100
     3.3 @@ -301,7 +301,7 @@
     3.4        run_thy name path;
     3.5        writeln ("**** Finished theory " ^ quote name ^ " ****\n")))
     3.6    else run_thy name path;
     3.7 -  Context.context (ThyInfo.get_theory name);
     3.8 +  Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name)));
     3.9    if ml then try_ml_file name time else ());
    3.10  
    3.11  end;
    3.12 @@ -313,7 +313,7 @@
    3.13  (* main loop *)
    3.14  
    3.15  fun gen_loop term no_pos =
    3.16 - (Context.reset_context ();
    3.17 + (Context.set_context NONE;
    3.18    Toplevel.loop (isar term no_pos));
    3.19  
    3.20  fun gen_main term no_pos =
     4.1 --- a/src/Pure/Isar/proof_display.ML	Fri Jan 19 13:09:32 2007 +0100
     4.2 +++ b/src/Pure/Isar/proof_display.ML	Fri Jan 19 13:09:33 2007 +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 -    Context.setmp (SOME (ProofContext.theory_of ctxt))
     4.8 +    Context.setmp (SOME (Context.Proof ctxt))
     4.9        (Present.results kind) (name_results name res));
    4.10  
    4.11  end;
     5.1 --- a/src/Pure/Thy/thm_database.ML	Fri Jan 19 13:09:32 2007 +0100
     5.2 +++ b/src/Pure/Thy/thm_database.ML	Fri Jan 19 13:09:33 2007 +0100
     5.3 @@ -99,7 +99,8 @@
     5.4      |> cat_lines
     5.5    end;
     5.6  
     5.7 -fun use_legacy_bindings thy = Context.use_mltext (legacy_bindings thy) true (SOME thy);
     5.8 +fun use_legacy_bindings thy =
     5.9 +  Context.use_mltext (legacy_bindings thy) true (SOME (Context.Theory thy));
    5.10  
    5.11  end;
    5.12  
     6.1 --- a/src/Pure/Thy/thy_info.ML	Fri Jan 19 13:09:32 2007 +0100
     6.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Jan 19 13:09:33 2007 +0100
     6.3 @@ -261,7 +261,7 @@
     6.4    | provide _ _ _ NONE = NONE;
     6.5  
     6.6  fun run_file path =
     6.7 -  (case Option.map Context.theory_name (Context.get_context ()) of
     6.8 +  (case Option.map (Context.theory_name o Context.the_theory) (Context.get_context ()) of
     6.9      NONE => (ThyLoad.load_file NONE path; ())
    6.10    | SOME name => (case lookup_deps name of
    6.11        SOME deps => change_deps name (provide path name
    6.12 @@ -382,7 +382,7 @@
    6.13  
    6.14  fun gen_use_thy' req prfx s = Output.toplevel_errors (fn () =>
    6.15    let val (_, (_, name)) = req [] prfx ([], s)
    6.16 -  in Context.context (get_theory name) end) ();
    6.17 +  in Context.set_context (SOME (Context.Theory (get_theory name))) end) ();
    6.18  
    6.19  fun gen_use_thy req = gen_use_thy' req Path.current;
    6.20  
    6.21 @@ -444,7 +444,9 @@
    6.22      val _ = change_thys (update_node name bparents (deps, SOME (Theory.copy theory)));
    6.23      val theory' = theory |> present dir' name bparents uses;
    6.24      val _ = put_theory name (Theory.copy theory');
    6.25 -    val ((), theory'') = Context.pass_theory theory' (List.app (load_file false)) uses_now;
    6.26 +    val ((), theory'') =
    6.27 +      Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now
    6.28 +      ||> Context.the_theory;
    6.29      val _ = put_theory name (Theory.copy theory'');
    6.30    in theory'' end;
    6.31  
     7.1 --- a/src/Pure/pure_thy.ML	Fri Jan 19 13:09:32 2007 +0100
     7.2 +++ b/src/Pure/pure_thy.ML	Fri Jan 19 13:09:33 2007 +0100
     7.3 @@ -506,7 +506,9 @@
     7.4  (* generic_setup *)
     7.5  
     7.6  fun generic_setup NONE = (fn thy => thy |> Context.setup ())
     7.7 -  | generic_setup (SOME txt) = Context.use_let "val setup: theory -> theory" "setup" txt;
     7.8 +  | generic_setup (SOME txt) =
     7.9 +      Context.use_let "val setup: theory -> theory" "Context.map_theory setup" txt
    7.10 +      |> Context.theory_map;
    7.11  
    7.12  
    7.13  (* add_oracle *)
    7.14 @@ -524,7 +526,8 @@
    7.15      \in\n\
    7.16      \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
    7.17      \end;\n";
    7.18 -  in Context.use_mltext_theory txt false end;
    7.19 +  in Context.use_mltext_update txt false end
    7.20 +  |> Context.theory_map;
    7.21  
    7.22  
    7.23  
     8.1 --- a/src/Pure/sign.ML	Fri Jan 19 13:09:32 2007 +0100
     8.2 +++ b/src/Pure/sign.ML	Fri Jan 19 13:09:33 2007 +0100
     8.3 @@ -840,31 +840,37 @@
     8.4  fun parse_ast_translation (a, txt) =
     8.5    txt |> Context.use_let ("val parse_ast_translation: (string * (" ^ advancedT a ^
     8.6        "Syntax.ast list -> Syntax.ast)) list")
     8.7 -    ("Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], [])");
     8.8 +    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
     8.9 +  |> Context.theory_map;
    8.10  
    8.11  fun parse_translation (a, txt) =
    8.12    txt |> Context.use_let ("val parse_translation: (string * (" ^ advancedT a ^
    8.13        "term list -> term)) list")
    8.14 -    ("Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], [])");
    8.15 +    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
    8.16 +  |> Context.theory_map;
    8.17  
    8.18  fun print_translation (a, txt) =
    8.19    txt |> Context.use_let ("val print_translation: (string * (" ^ advancedT a ^
    8.20        "term list -> term)) list")
    8.21 -    ("Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, [])");
    8.22 +    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
    8.23 +  |> Context.theory_map;
    8.24  
    8.25  fun print_ast_translation (a, txt) =
    8.26    txt |> Context.use_let ("val print_ast_translation: (string * (" ^ advancedT a ^
    8.27        "Syntax.ast list -> Syntax.ast)) list")
    8.28 -    ("Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation)");
    8.29 +    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
    8.30 +  |> Context.theory_map;
    8.31  
    8.32  fun typed_print_translation (a, txt) =
    8.33    txt |> Context.use_let ("val typed_print_translation: (string * (" ^ advancedT a ^
    8.34        "bool -> typ -> term list -> term)) list")
    8.35 -    ("Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation");
    8.36 +    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
    8.37 +  |> Context.theory_map;
    8.38  
    8.39  val token_translation =
    8.40    Context.use_let "val token_translation: (string * string * (string -> string * real)) list"
    8.41 -    "Sign.add_tokentrfuns token_translation";
    8.42 +    "Context.map_theory (Sign.add_tokentrfuns token_translation)"
    8.43 +  #> Context.theory_map;
    8.44  
    8.45  end;
    8.46