# HG changeset patch
# User wenzelm
# Date 1169240882 -3600
# Node ID 07875394618e5a65670ea21f163157e472e54b2b
# Parent  008794185f4dcfe5330df1b95c185faadc65598c
moved ML context stuff to from Context to ML_Context;

diff -r 008794185f4d -r 07875394618e doc-src/IsarImplementation/Thy/integration.thy
--- a/doc-src/IsarImplementation/Thy/integration.thy	Fri Jan 19 22:08:01 2007 +0100
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Fri Jan 19 22:08:02 2007 +0100
@@ -241,7 +241,7 @@
 text %mlref {*
   \begin{mldecls}
   @{index_ML the_context: "unit -> theory"} \\
-  @{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
+  @{index_ML "ML_Context.>> ": "(theory -> theory) -> unit"} \\
   \end{mldecls}
 
   \begin{description}
@@ -255,7 +255,7 @@
   information immediately, or produce an explicit @{ML_type
   theory_ref} (cf.\ \secref{sec:context-theory}).
 
-  \item @{ML "Context.>>"}~@{text f} applies theory transformation
+  \item @{ML "ML_Context.>>"}~@{text f} applies theory transformation
   @{text f} to the current theory of the {\ML} toplevel.  In order to
   work as expected, the theory should be still under construction, and
   the Isar language element that invoked the {\ML} compiler in the
diff -r 008794185f4d -r 07875394618e src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Fri Jan 19 22:08:01 2007 +0100
+++ b/src/Provers/clasimp.ML	Fri Jan 19 22:08:02 2007 +0100
@@ -81,7 +81,7 @@
     Simplifier.change_simpset_of thy (fn _ => ss')
   end;
 
-fun change_clasimpset f = change_clasimpset_of (Context.the_context ()) f;
+fun change_clasimpset f = change_clasimpset_of (ML_Context.the_context ()) f;
 fun clasimpset () = (Classical.claset (), Simplifier.simpset ());
 
 
diff -r 008794185f4d -r 07875394618e src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Jan 19 22:08:01 2007 +0100
+++ b/src/Provers/classical.ML	Fri Jan 19 22:08:02 2007 +0100
@@ -879,12 +879,12 @@
   (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
 
 val change_claset_of = change o #1 o GlobalClaset.get;
-fun change_claset f = change_claset_of (Context.the_context ()) f;
+fun change_claset f = change_claset_of (ML_Context.the_context ()) f;
 
 fun claset_of thy =
   let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
   in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
-val claset = claset_of o Context.the_context;
+val claset = claset_of o ML_Context.the_context;
 
 fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
 fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;
diff -r 008794185f4d -r 07875394618e src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Fri Jan 19 22:08:01 2007 +0100
+++ b/src/Pure/Isar/proof_display.ML	Fri Jan 19 22:08:02 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 (Context.Proof ctxt))
+    ML_Context.setmp (SOME (Context.Proof ctxt))
       (Present.results kind) (name_results name res));
 
 end;
diff -r 008794185f4d -r 07875394618e src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Jan 19 22:08:01 2007 +0100
+++ b/src/Pure/Isar/toplevel.ML	Fri Jan 19 22:08:02 2007 +0100
@@ -267,7 +267,7 @@
 local
 
 fun with_context f xs =
-  (case Context.get_context () of NONE => []
+  (case ML_Context.get_context () of NONE => []
   | SOME context => map (f (Context.proof_of context)) xs);
 
 fun raised name [] = "exception " ^ name ^ " raised"
diff -r 008794185f4d -r 07875394618e src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Fri Jan 19 22:08:01 2007 +0100
+++ b/src/Pure/Thy/thm_database.ML	Fri Jan 19 22:08:02 2007 +0100
@@ -100,7 +100,7 @@
   end;
 
 fun use_legacy_bindings thy =
-  Context.use_mltext (legacy_bindings thy) true (SOME (Context.Theory thy));
+  ML_Context.use_mltext (legacy_bindings thy) true (SOME (Context.Theory thy));
 
 end;
 
diff -r 008794185f4d -r 07875394618e src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Jan 19 22:08:01 2007 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Jan 19 22:08:02 2007 +0100
@@ -261,7 +261,7 @@
   | provide _ _ _ NONE = NONE;
 
 fun run_file path =
-  (case Option.map (Context.theory_name o Context.the_theory) (Context.get_context ()) of
+  (case Option.map (Context.theory_name o Context.the_theory) (ML_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.set_context (SOME (Context.Theory (get_theory name))) end) ();
+  in ML_Context.set_context (SOME (Context.Theory (get_theory name))) end) ();
 
 fun gen_use_thy req = gen_use_thy' req Path.current;
 
@@ -445,7 +445,7 @@
     val theory' = theory |> present dir' name bparents uses;
     val _ = put_theory name (Theory.copy theory');
     val ((), theory'') =
-      Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now
+      ML_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 008794185f4d -r 07875394618e src/Pure/context.ML
--- a/src/Pure/context.ML	Fri Jan 19 22:08:01 2007 +0100
+++ b/src/Pure/context.ML	Fri Jan 19 22:08:02 2007 +0100
@@ -3,8 +3,8 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Generic theory contexts with unique identity, arbitrarily typed data,
-development graph and history support.  Implicit theory contexts in ML.
-Generic proof contexts with arbitrarily typed data.
+development graph and history support. Generic proof contexts with
+arbitrarily typed data.
 *)
 
 signature BASIC_CONTEXT =
@@ -12,7 +12,6 @@
   type theory
   type theory_ref
   exception THEORY of string * theory list
-  val the_context: unit -> theory
 end;
 
 signature CONTEXT =
@@ -67,19 +66,7 @@
   val proof_map: (generic -> generic) -> proof -> proof
   val theory_of: generic -> theory   (*total*)
   val proof_of: generic -> proof     (*total*)
-  (*ML context*)
-  val get_context: unit -> generic option
-  val set_context: generic option -> unit
-  val setmp: generic option -> ('a -> 'b) -> 'a -> 'b
-  val the_generic_context: unit -> generic
-  val the_local_context: unit -> proof
-  val pass: generic option -> ('a -> 'b) -> 'a -> 'b * generic option
-  val pass_context: generic -> ('a -> 'b) -> 'a -> 'b * generic
-  val save: ('a -> 'b) -> 'a -> 'b
-  val >> : (theory -> theory) -> unit
-  val use_mltext: string -> bool -> generic option -> unit
-  val use_mltext_update: string -> bool -> generic -> generic
-  val use_let: string -> string -> string -> generic -> generic
+  (*delayed setup*)
   val add_setup: (theory -> theory) -> unit
   val setup: unit -> theory -> theory
 end;
@@ -543,57 +530,7 @@
 
 
 
-(*** ML context ***)
-
-local
-  val current_context = ref (NONE: generic option);
-in
-  fun get_context () = ! current_context;
-  fun set_context opt_context = current_context := opt_context;
-  fun setmp opt_context f x = Library.setmp current_context opt_context f x;
-end;
-
-fun the_generic_context () =
-  (case get_context () of
-    SOME context => context
-  | _ => error "Unknown context");
-
-val the_context = theory_of o the_generic_context;
-val the_local_context = the_proof o the_generic_context;
-
-fun pass opt_context f x =
-  setmp opt_context (fn x => let val y = f x in (y, get_context ()) end) x;
-
-fun pass_context context f x =
-  (case pass (SOME context) f x of
-    (y, SOME context') => (y, context')
-  | (_, NONE) => error "Lost context in ML");
-
-fun save f x = setmp (get_context ()) f x;
-
-
-(* map context *)
-
-nonfix >>;
-fun >> f = set_context (SOME (map_theory f (the_generic_context ())));
-
-
-(* use ML text *)
-
-fun use_output verbose txt =
-  Output.ML_errors (use_text Output.ml_output verbose) (Symbol.escape txt);
-
-fun use_mltext txt verbose opt_context = setmp opt_context (fn () => use_output verbose txt) ();
-fun use_mltext_update txt verbose context = #2 (pass_context context (use_output verbose) txt);
-
-fun use_context txt = use_mltext_update
-    ("Context.set_context (SOME ((" ^ txt ^ ") (Context.the_generic_context ())));") false;
-
-fun use_let bind body txt =
-  use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
-
-
-(* delayed theory setup *)
+(** delayed theory setup **)
 
 local
   val setup_fn = ref (I: theory -> theory);
diff -r 008794185f4d -r 07875394618e src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri Jan 19 22:08:01 2007 +0100
+++ b/src/Pure/simplifier.ML	Fri Jan 19 22:08:02 2007 +0100
@@ -104,10 +104,10 @@
 val get_simpset = ! o GlobalSimpset.get;
 
 val change_simpset_of = change o GlobalSimpset.get;
-fun change_simpset f = change_simpset_of (Context.the_context ()) f;
+fun change_simpset f = change_simpset_of (ML_Context.the_context ()) f;
 
 fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_simpset thy);
-val simpset = simpset_of o Context.the_context;
+val simpset = simpset_of o ML_Context.the_context;
 
 
 fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;