# HG changeset patch
# User wenzelm
# Date 957556817 -7200
# Node ID e1c36f2c02c02bee5850393b2232297a031e0665
# Parent  de0e9f689c6e19928e6c49fa15e6588ec4cd1601
GPLed;
improved begin_theory: proper presentation if 'files' change theory;

diff -r de0e9f689c6e -r e1c36f2c02c0 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri May 05 21:59:28 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML	Fri May 05 22:00:17 2000 +0200
@@ -1,6 +1,7 @@
 (*  Title:      Pure/Thy/thy_info.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
 Theory loader database, including theory and file dependencies.
 *)
@@ -40,8 +41,8 @@
   val load_file: bool -> Path.T -> unit
   val use: string -> unit
   val quiet_update_thy: bool -> string -> unit
-  val begin_theory: string -> string list -> (Path.T * bool) list -> theory
-  val begin_update_theory: string -> string list -> (Path.T * bool) list -> theory
+  val begin_theory: (string -> string list -> (Path.T * bool) list -> theory -> theory) ->
+    bool -> string -> string list -> (Path.T * bool) list -> theory
   val end_theory: theory -> theory
   val finish: unit -> unit
   val register_theory: theory -> unit
@@ -370,8 +371,9 @@
 
 (* begin / end theory *)
 
-fun gen_begin_theory assert_thy name parents paths =
+fun begin_theory present upd name parents paths =
   let
+    val assert_thy = if upd then quiet_update_thy true else weak_use_thy;
     val _ = check_unfinished error name;
     val _ = (map Path.basic parents; seq assert_thy parents);
     val theory = PureThy.begin_theory name (map get_theory parents);
@@ -380,10 +382,9 @@
       else (init_deps None (map #1 paths));   (*records additional ML files only!*)
     val _ = change_thys (update_node name parents (deps, Some theory));
     val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;
-  in Context.setmp (Some theory) (seq (load_file false)) use_paths; theory end;
-
-val begin_theory = gen_begin_theory weak_use_thy;
-val begin_update_theory = gen_begin_theory (quiet_update_thy true);
+    val theory' = theory |> present name parents paths;
+    val ((), theory'') = Context.pass_theory theory' (seq (load_file false)) use_paths;
+  in theory'' end;
 
 fun end_theory theory =
   let