# HG changeset patch
# User wenzelm
# Date 920978404 -3600
# Node ID fb7b8d6c2bd1f4f9204e45061b5133f003567311
# Parent  e1faf0f6f2b85af2ef14b218a08137dfa8bad542
begin/end_theory: presentation;

diff -r e1faf0f6f2b8 -r fb7b8d6c2bd1 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Mar 09 12:19:25 1999 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Tue Mar 09 12:20:04 1999 +0100
@@ -57,6 +57,8 @@
   val print_ast_translation: string -> theory -> theory
   val token_translation: string -> theory -> theory
   val add_oracle: bstring * string -> theory -> theory
+  val begin_theory: string -> string list -> (string * bool) list -> theory
+  val end_theory: theory -> theory
   val theory: string * string list * (string * bool) list
     -> Toplevel.transition -> Toplevel.transition
   val context: string -> Toplevel.transition -> Toplevel.transition
@@ -174,8 +176,8 @@
 
 (* use ML text *)
 
-fun use_mltext txt opt_thy = #2 (Context.fetch opt_thy (use_text false) txt);
-fun use_mltext_theory txt thy = #2 (Context.fetch_theory thy (use_text false) txt);
+fun use_mltext txt opt_thy = #2 (Context.pass opt_thy (use_text false) txt);
+fun use_mltext_theory txt thy = #2 (Context.pass_theory thy (use_text false) txt);
 
 fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");");
 
@@ -222,21 +224,31 @@
     ("(" ^ quote name ^ ", " ^ txt ^ ")");
 
 
-(* theory init and exit *)
+(* theory init and exit *)	(* FIXME move? rearrange? *)
 
-fun begin_theory (name, parents, files) () =
+fun begin_theory name parents files =
   let
-    val thy = ThyInfo.begin_theory name parents;
-    val names = mapfilter (fn (x, true) => Some x | _ => None) files;
-  in Context.setmp (Some thy) (seq ThyInfo.use) names; thy end;
+    val paths = map (apfst Path.unpack) files;
+    val thy = ThyInfo.begin_theory name parents paths;
+  in Present.begin_theory name parents paths; thy end;
 
+
+(* FIXME
 fun end_theory thy =
   let val thy' = PureThy.end_theory thy in
+    Present.end_theory (PureThy.get_name thy');
     transform_error ThyInfo.put_theory thy'
       handle exn => raise PureThy.ROLLBACK (thy', Some exn)     (* FIXME !!?? *)
   end;
+*)
 
-fun theory spec = Toplevel.init_theory (begin_theory spec) end_theory;
+fun end_theory thy =
+  (Present.end_theory (PureThy.get_name thy); ThyInfo.end_theory thy);
+
+fun bg_theory (name, parents, files) () = begin_theory name parents files;
+fun en_theory thy = (end_theory thy; ());
+
+fun theory spec = Toplevel.init_theory (bg_theory spec) en_theory;
 
 
 (* context switch *)