1.1 --- a/doc-src/IsarImplementation/Thy/integration.thy	Fri Jan 19 22:08:01 2007 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/integration.thy	Fri Jan 19 22:08:02 2007 +0100
     1.3 @@ -241,7 +241,7 @@
     1.4  text %mlref {*
     1.5    \begin{mldecls}
     1.6    @{index_ML the_context: "unit -> theory"} \\
     1.7 -  @{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
     1.8 +  @{index_ML "ML_Context.>> ": "(theory -> theory) -> unit"} \\
     1.9    \end{mldecls}
    1.10  
    1.11    \begin{description}
    1.12 @@ -255,7 +255,7 @@
    1.13    information immediately, or produce an explicit @{ML_type
    1.14    theory_ref} (cf.\ \secref{sec:context-theory}).
    1.15  
    1.16 -  \item @{ML "Context.>>"}~@{text f} applies theory transformation
    1.17 +  \item @{ML "ML_Context.>>"}~@{text f} applies theory transformation
    1.18    @{text f} to the current theory of the {\ML} toplevel.  In order to
    1.19    work as expected, the theory should be still under construction, and
    1.20    the Isar language element that invoked the {\ML} compiler in the

     2.1 --- a/src/Provers/clasimp.ML	Fri Jan 19 22:08:01 2007 +0100
     2.2 +++ b/src/Provers/clasimp.ML	Fri Jan 19 22:08:02 2007 +0100
     2.3 @@ -81,7 +81,7 @@
     2.4      Simplifier.change_simpset_of thy (fn _ => ss')
     2.5    end;
     2.6  
     2.7 -fun change_clasimpset f = change_clasimpset_of (Context.the_context ()) f;
     2.8 +fun change_clasimpset f = change_clasimpset_of (ML_Context.the_context ()) f;
     2.9  fun clasimpset () = (Classical.claset (), Simplifier.simpset ());
    2.10  
    2.11  

     3.1 --- a/src/Provers/classical.ML	Fri Jan 19 22:08:01 2007 +0100
     3.2 +++ b/src/Provers/classical.ML	Fri Jan 19 22:08:02 2007 +0100
     3.3 @@ -879,12 +879,12 @@
     3.4    (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
     3.5  
     3.6  val change_claset_of = change o #1 o GlobalClaset.get;
     3.7 -fun change_claset f = change_claset_of (Context.the_context ()) f;
     3.8 +fun change_claset f = change_claset_of (ML_Context.the_context ()) f;
     3.9  
    3.10  fun claset_of thy =
    3.11    let val (cs_ref, ctxt_cs) = GlobalClaset.get thy
    3.12    in context_cs (ProofContext.init thy) (! cs_ref) (ctxt_cs) end;
    3.13 -val claset = claset_of o Context.the_context;
    3.14 +val claset = claset_of o ML_Context.the_context;
    3.15  
    3.16  fun CLASET tacf st = tacf (claset_of (Thm.theory_of_thm st)) st;
    3.17  fun CLASET' tacf i st = tacf (claset_of (Thm.theory_of_thm st)) i st;

     4.1 --- a/src/Pure/Isar/proof_display.ML	Fri Jan 19 22:08:01 2007 +0100
     4.2 +++ b/src/Pure/Isar/proof_display.ML	Fri Jan 19 22:08:02 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 (Context.Proof ctxt))
     4.8 +    ML_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/Isar/toplevel.ML	Fri Jan 19 22:08:01 2007 +0100
     5.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Jan 19 22:08:02 2007 +0100
     5.3 @@ -267,7 +267,7 @@
     5.4  local
     5.5  
     5.6  fun with_context f xs =
     5.7 -  (case Context.get_context () of NONE => []
     5.8 +  (case ML_Context.get_context () of NONE => []
     5.9    | SOME context => map (f (Context.proof_of context)) xs);
    5.10  
    5.11  fun raised name [] = "exception " ^ name ^ " raised"

     6.1 --- a/src/Pure/Thy/thm_database.ML	Fri Jan 19 22:08:01 2007 +0100
     6.2 +++ b/src/Pure/Thy/thm_database.ML	Fri Jan 19 22:08:02 2007 +0100
     6.3 @@ -100,7 +100,7 @@
     6.4    end;
     6.5  
     6.6  fun use_legacy_bindings thy =
     6.7 -  Context.use_mltext (legacy_bindings thy) true (SOME (Context.Theory thy));
     6.8 +  ML_Context.use_mltext (legacy_bindings thy) true (SOME (Context.Theory thy));
     6.9  
    6.10  end;
    6.11  

     7.1 --- a/src/Pure/Thy/thy_info.ML	Fri Jan 19 22:08:01 2007 +0100
     7.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Jan 19 22:08:02 2007 +0100
     7.3 @@ -261,7 +261,7 @@
     7.4    | provide _ _ _ NONE = NONE;
     7.5  
     7.6  fun run_file path =
     7.7 -  (case Option.map (Context.theory_name o Context.the_theory) (Context.get_context ()) of
     7.8 +  (case Option.map (Context.theory_name o Context.the_theory) (ML_Context.get_context ()) of
     7.9      NONE => (ThyLoad.load_file NONE path; ())
    7.10    | SOME name => (case lookup_deps name of
    7.11        SOME deps => change_deps name (provide path name
    7.12 @@ -382,7 +382,7 @@
    7.13  
    7.14  fun gen_use_thy' req prfx s = Output.toplevel_errors (fn () =>
    7.15    let val (_, (_, name)) = req [] prfx ([], s)
    7.16 -  in Context.set_context (SOME (Context.Theory (get_theory name))) end) ();
    7.17 +  in ML_Context.set_context (SOME (Context.Theory (get_theory name))) end) ();
    7.18  
    7.19  fun gen_use_thy req = gen_use_thy' req Path.current;
    7.20  
    7.21 @@ -445,7 +445,7 @@
    7.22      val theory' = theory |> present dir' name bparents uses;
    7.23      val _ = put_theory name (Theory.copy theory');
    7.24      val ((), theory'') =
    7.25 -      Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now
    7.26 +      ML_Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now
    7.27        ||> Context.the_theory;
    7.28      val _ = put_theory name (Theory.copy theory'');
    7.29    in theory'' end;

     8.1 --- a/src/Pure/context.ML	Fri Jan 19 22:08:01 2007 +0100
     8.2 +++ b/src/Pure/context.ML	Fri Jan 19 22:08:02 2007 +0100
     8.3 @@ -3,8 +3,8 @@
     8.4      Author:     Markus Wenzel, TU Muenchen
     8.5  
     8.6  Generic theory contexts with unique identity, arbitrarily typed data,
     8.7 -development graph and history support.  Implicit theory contexts in ML.
     8.8 -Generic proof contexts with arbitrarily typed data.
     8.9 +development graph and history support. Generic proof contexts with
    8.10 +arbitrarily typed data.
    8.11  *)
    8.12  
    8.13  signature BASIC_CONTEXT =
    8.14 @@ -12,7 +12,6 @@
    8.15    type theory
    8.16    type theory_ref
    8.17    exception THEORY of string * theory list
    8.18 -  val the_context: unit -> theory
    8.19  end;
    8.20  
    8.21  signature CONTEXT =
    8.22 @@ -67,19 +66,7 @@
    8.23    val proof_map: (generic -> generic) -> proof -> proof
    8.24    val theory_of: generic -> theory   (*total*)
    8.25    val proof_of: generic -> proof     (*total*)
    8.26 -  (*ML context*)
    8.27 -  val get_context: unit -> generic option
    8.28 -  val set_context: generic option -> unit
    8.29 -  val setmp: generic option -> ('a -> 'b) -> 'a -> 'b
    8.30 -  val the_generic_context: unit -> generic
    8.31 -  val the_local_context: unit -> proof
    8.32 -  val pass: generic option -> ('a -> 'b) -> 'a -> 'b * generic option
    8.33 -  val pass_context: generic -> ('a -> 'b) -> 'a -> 'b * generic
    8.34 -  val save: ('a -> 'b) -> 'a -> 'b
    8.35 -  val >> : (theory -> theory) -> unit
    8.36 -  val use_mltext: string -> bool -> generic option -> unit
    8.37 -  val use_mltext_update: string -> bool -> generic -> generic
    8.38 -  val use_let: string -> string -> string -> generic -> generic
    8.39 +  (*delayed setup*)
    8.40    val add_setup: (theory -> theory) -> unit
    8.41    val setup: unit -> theory -> theory
    8.42  end;
    8.43 @@ -543,57 +530,7 @@
    8.44  
    8.45  
    8.46  
    8.47 -(*** ML context ***)
    8.48 -
    8.49 -local
    8.50 -  val current_context = ref (NONE: generic option);
    8.51 -in
    8.52 -  fun get_context () = ! current_context;
    8.53 -  fun set_context opt_context = current_context := opt_context;
    8.54 -  fun setmp opt_context f x = Library.setmp current_context opt_context f x;
    8.55 -end;
    8.56 -
    8.57 -fun the_generic_context () =
    8.58 -  (case get_context () of
    8.59 -    SOME context => context
    8.60 -  | _ => error "Unknown context");
    8.61 -
    8.62 -val the_context = theory_of o the_generic_context;
    8.63 -val the_local_context = the_proof o the_generic_context;
    8.64 -
    8.65 -fun pass opt_context f x =
    8.66 -  setmp opt_context (fn x => let val y = f x in (y, get_context ()) end) x;
    8.67 -
    8.68 -fun pass_context context f x =
    8.69 -  (case pass (SOME context) f x of
    8.70 -    (y, SOME context') => (y, context')
    8.71 -  | (_, NONE) => error "Lost context in ML");
    8.72 -
    8.73 -fun save f x = setmp (get_context ()) f x;
    8.74 -
    8.75 -
    8.76 -(* map context *)
    8.77 -
    8.78 -nonfix >>;
    8.79 -fun >> f = set_context (SOME (map_theory f (the_generic_context ())));
    8.80 -
    8.81 -
    8.82 -(* use ML text *)
    8.83 -
    8.84 -fun use_output verbose txt =
    8.85 -  Output.ML_errors (use_text Output.ml_output verbose) (Symbol.escape txt);
    8.86 -
    8.87 -fun use_mltext txt verbose opt_context = setmp opt_context (fn () => use_output verbose txt) ();
    8.88 -fun use_mltext_update txt verbose context = #2 (pass_context context (use_output verbose) txt);
    8.89 -
    8.90 -fun use_context txt = use_mltext_update
    8.91 -    ("Context.set_context (SOME ((" ^ txt ^ ") (Context.the_generic_context ())));") false;
    8.92 -
    8.93 -fun use_let bind body txt =
    8.94 -  use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
    8.95 -
    8.96 -
    8.97 -(* delayed theory setup *)
    8.98 +(** delayed theory setup **)
    8.99  
   8.100  local
   8.101    val setup_fn = ref (I: theory -> theory);

     9.1 --- a/src/Pure/simplifier.ML	Fri Jan 19 22:08:01 2007 +0100
     9.2 +++ b/src/Pure/simplifier.ML	Fri Jan 19 22:08:02 2007 +0100
     9.3 @@ -104,10 +104,10 @@
     9.4  val get_simpset = ! o GlobalSimpset.get;
     9.5  
     9.6  val change_simpset_of = change o GlobalSimpset.get;
     9.7 -fun change_simpset f = change_simpset_of (Context.the_context ()) f;
     9.8 +fun change_simpset f = change_simpset_of (ML_Context.the_context ()) f;
     9.9  
    9.10  fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_simpset thy);
    9.11 -val simpset = simpset_of o Context.the_context;
    9.12 +val simpset = simpset_of o ML_Context.the_context;
    9.13  
    9.14  
    9.15  fun SIMPSET tacf st = tacf (simpset_of (Thm.theory_of_thm st)) st;