# HG changeset patch
# User wenzelm
# Date 918245098 -3600
# Node ID 0aa2e536bc2087e665e8f92533bfc37ee8c73da7
# Parent  ebce4ebba491df8a72ad54d7319b6366471f327f
improved theory, context, update_context;

diff -r ebce4ebba491 -r 0aa2e536bc20 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Fri Feb 05 21:04:31 1999 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Fri Feb 05 21:04:58 1999 +0100
@@ -57,9 +57,10 @@
   val print_ast_translation: string -> theory -> theory
   val token_translation: string -> theory -> theory
   val add_oracle: bstring * string -> theory -> theory
-  val the_theory: string -> unit -> theory
-  val begin_theory: string * string list -> unit -> theory
-  val end_theory: theory -> unit
+  val theory: string * string list * (string * bool) list
+    -> Toplevel.transition -> Toplevel.transition
+  val context: string -> Toplevel.transition -> Toplevel.transition
+  val update_context: string -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure IsarThy: ISAR_THY =
@@ -239,9 +240,9 @@
 
 (* theory init and exit *)
 
-fun the_theory name () = ThyInfo.theory name;
-
-fun begin_theory (name, names) () = ThyInfo.begin_theory name names;
+fun begin_theory (name, parents, files) () =
+  let val thy = ThyInfo.begin_theory name parents
+  in seq ThyInfo.use (mapfilter (fn (x, true) => Some x | _ => None) files); thy end;
 
 fun end_theory thy =
   let val thy' = PureThy.end_theory thy in
@@ -249,5 +250,17 @@
       handle exn => raise PureThy.ROLLBACK (thy', Some exn)     (* FIXME !!?? *)
   end;
 
+fun theory spec = Toplevel.init_theory (begin_theory spec) end_theory;
+
+
+(* context switch *)
+
+fun switch_theory require name =
+  Toplevel.init_theory
+    (fn () => (Context.save require name; ThyInfo.get_theory name)) (K ());
+
+val context = switch_theory ThyInfo.use_thy;
+val update_context = switch_theory ThyInfo.update_thy;
+
 
 end;