# HG changeset patch
# User wenzelm
# Date 1169208573 -3600
# Node ID cf6019fece637e88b49a4a9e094ee0b5c5a7db1e
# Parent  c138cfd500f7f81c26bd154da0b5074adbd3e031
adapted ML context operations;

diff -r c138cfd500f7 -r cf6019fece63 src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Fri Jan 19 13:09:32 2007 +0100
+++ b/src/Pure/Isar/isar_output.ML	Fri Jan 19 13:09:33 2007 +0100
@@ -509,7 +509,7 @@
 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
 
 fun output_ml ml src ctxt txt =
- (Context.use_mltext (ml txt) false (SOME (ProofContext.theory_of ctxt));
+ (Context.use_mltext (ml txt) false (SOME (Context.Proof ctxt));
   (if ! source then str_of_source src else txt)
   |> (if ! quotes then quote else I)
   |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
diff -r c138cfd500f7 -r cf6019fece63 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Jan 19 13:09:32 2007 +0100
+++ b/src/Pure/Isar/method.ML	Fri Jan 19 13:09:33 2007 +0100
@@ -348,7 +348,7 @@
        ^ txt ^
        "\nend in Method.set_tactic tactic end")
     false NONE;
-    Context.setmp (SOME (ProofContext.theory_of ctxt)) (! tactic_ref ctxt) facts));
+    Context.setmp (SOME (Context.Proof ctxt)) (! tactic_ref ctxt) facts));
 
 
 
@@ -448,8 +448,9 @@
     "val thm = PureThy.get_thm_closure (Context.the_context ()) o PureThy.Name;\n\
     \val thms = PureThy.get_thms_closure (Context.the_context ()) o PureThy.Name;\n\
     \val method: bstring * (Method.src -> Proof.context -> Proof.method) * string"
-    "Method.add_method method"
-    ("(" ^ Library.quote name ^ ", " ^ txt ^ ", " ^ Library.quote cmt ^ ")");
+    "Context.map_theory (Method.add_method method)"
+    ("(" ^ quote name ^ ", " ^ txt ^ ", " ^ quote cmt ^ ")")
+  |> Context.theory_map;
 
 
 
diff -r c138cfd500f7 -r cf6019fece63 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Jan 19 13:09:32 2007 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Jan 19 13:09:33 2007 +0100
@@ -301,7 +301,7 @@
       run_thy name path;
       writeln ("**** Finished theory " ^ quote name ^ " ****\n")))
   else run_thy name path;
-  Context.context (ThyInfo.get_theory name);
+  Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name)));
   if ml then try_ml_file name time else ());
 
 end;
@@ -313,7 +313,7 @@
 (* main loop *)
 
 fun gen_loop term no_pos =
- (Context.reset_context ();
+ (Context.set_context NONE;
   Toplevel.loop (isar term no_pos));
 
 fun gen_main term no_pos =
diff -r c138cfd500f7 -r cf6019fece63 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Fri Jan 19 13:09:32 2007 +0100
+++ b/src/Pure/Isar/proof_display.ML	Fri Jan 19 13:09:33 2007 +0100
@@ -123,7 +123,7 @@
 fun present_results ctxt ((kind, name), res) =
   if kind = "" orelse kind = Thm.internalK then ()
   else (print_results true ctxt ((kind, name), res);
-    Context.setmp (SOME (ProofContext.theory_of ctxt))
+    Context.setmp (SOME (Context.Proof ctxt))
       (Present.results kind) (name_results name res));
 
 end;
diff -r c138cfd500f7 -r cf6019fece63 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Fri Jan 19 13:09:32 2007 +0100
+++ b/src/Pure/Thy/thm_database.ML	Fri Jan 19 13:09:33 2007 +0100
@@ -99,7 +99,8 @@
     |> cat_lines
   end;
 
-fun use_legacy_bindings thy = Context.use_mltext (legacy_bindings thy) true (SOME thy);
+fun use_legacy_bindings thy =
+  Context.use_mltext (legacy_bindings thy) true (SOME (Context.Theory thy));
 
 end;
 
diff -r c138cfd500f7 -r cf6019fece63 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Jan 19 13:09:32 2007 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Jan 19 13:09:33 2007 +0100
@@ -261,7 +261,7 @@
   | provide _ _ _ NONE = NONE;
 
 fun run_file path =
-  (case Option.map Context.theory_name (Context.get_context ()) of
+  (case Option.map (Context.theory_name o Context.the_theory) (Context.get_context ()) of
     NONE => (ThyLoad.load_file NONE path; ())
   | SOME name => (case lookup_deps name of
       SOME deps => change_deps name (provide path name
@@ -382,7 +382,7 @@
 
 fun gen_use_thy' req prfx s = Output.toplevel_errors (fn () =>
   let val (_, (_, name)) = req [] prfx ([], s)
-  in Context.context (get_theory name) end) ();
+  in Context.set_context (SOME (Context.Theory (get_theory name))) end) ();
 
 fun gen_use_thy req = gen_use_thy' req Path.current;
 
@@ -444,7 +444,9 @@
     val _ = change_thys (update_node name bparents (deps, SOME (Theory.copy theory)));
     val theory' = theory |> present dir' name bparents uses;
     val _ = put_theory name (Theory.copy theory');
-    val ((), theory'') = Context.pass_theory theory' (List.app (load_file false)) uses_now;
+    val ((), theory'') =
+      Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now
+      ||> Context.the_theory;
     val _ = put_theory name (Theory.copy theory'');
   in theory'' end;
 
diff -r c138cfd500f7 -r cf6019fece63 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Jan 19 13:09:32 2007 +0100
+++ b/src/Pure/pure_thy.ML	Fri Jan 19 13:09:33 2007 +0100
@@ -506,7 +506,9 @@
 (* generic_setup *)
 
 fun generic_setup NONE = (fn thy => thy |> Context.setup ())
-  | generic_setup (SOME txt) = Context.use_let "val setup: theory -> theory" "setup" txt;
+  | generic_setup (SOME txt) =
+      Context.use_let "val setup: theory -> theory" "Context.map_theory setup" txt
+      |> Context.theory_map;
 
 
 (* add_oracle *)
@@ -524,7 +526,8 @@
     \in\n\
     \  fun " ^ name ^ " thy x = invoke_" ^ name ^ " (thy, Arg x);\n\
     \end;\n";
-  in Context.use_mltext_theory txt false end;
+  in Context.use_mltext_update txt false end
+  |> Context.theory_map;
 
 
 
diff -r c138cfd500f7 -r cf6019fece63 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Jan 19 13:09:32 2007 +0100
+++ b/src/Pure/sign.ML	Fri Jan 19 13:09:33 2007 +0100
@@ -840,31 +840,37 @@
 fun parse_ast_translation (a, txt) =
   txt |> Context.use_let ("val parse_ast_translation: (string * (" ^ advancedT a ^
       "Syntax.ast list -> Syntax.ast)) list")
-    ("Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], [])");
+    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns (parse_ast_translation, [], [], []))")
+  |> Context.theory_map;
 
 fun parse_translation (a, txt) =
   txt |> Context.use_let ("val parse_translation: (string * (" ^ advancedT a ^
       "term list -> term)) list")
-    ("Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], [])");
+    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], parse_translation, [], []))")
+  |> Context.theory_map;
 
 fun print_translation (a, txt) =
   txt |> Context.use_let ("val print_translation: (string * (" ^ advancedT a ^
       "term list -> term)) list")
-    ("Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, [])");
+    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], print_translation, []))")
+  |> Context.theory_map;
 
 fun print_ast_translation (a, txt) =
   txt |> Context.use_let ("val print_ast_translation: (string * (" ^ advancedT a ^
       "Syntax.ast list -> Syntax.ast)) list")
-    ("Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation)");
+    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfuns ([], [], [], print_ast_translation))")
+  |> Context.theory_map;
 
 fun typed_print_translation (a, txt) =
   txt |> Context.use_let ("val typed_print_translation: (string * (" ^ advancedT a ^
       "bool -> typ -> term list -> term)) list")
-    ("Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation");
+    ("Context.map_theory (Sign.add_" ^ advancedN a ^ "trfunsT typed_print_translation)")
+  |> Context.theory_map;
 
 val token_translation =
   Context.use_let "val token_translation: (string * string * (string -> string * real)) list"
-    "Sign.add_tokentrfuns token_translation";
+    "Context.map_theory (Sign.add_tokentrfuns token_translation)"
+  #> Context.theory_map;
 
 end;