begin_update_theory;
authorwenzelm
Tue Aug 17 22:19:25 1999 +0200 (1999-08-17 ago)
changeset 7242f17f2e8ba0c7
parent 7241 8f3c14d60345
child 7243 886ecd6a27ac
begin_update_theory;
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Aug 17 22:16:21 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Aug 17 22:19:25 1999 +0200
     1.3 @@ -458,12 +458,15 @@
     1.4  
     1.5  (* theory init and exit *)
     1.6  
     1.7 -fun begin_theory name parents files =
     1.8 +fun gen_begin_theory bg name parents files =
     1.9    let
    1.10      val paths = map (apfst Path.unpack) files;
    1.11 -    val thy = ThyInfo.begin_theory name parents paths;
    1.12 +    val thy = bg name parents paths;
    1.13    in Present.begin_theory name parents paths thy end;
    1.14  
    1.15 +val begin_theory = gen_begin_theory ThyInfo.begin_theory;
    1.16 +val begin_update_theory = gen_begin_theory ThyInfo.begin_update_theory;
    1.17 +
    1.18  fun end_theory thy =
    1.19    (Present.end_theory (PureThy.get_name thy); ThyInfo.end_theory thy);
    1.20  
    1.21 @@ -471,8 +474,7 @@
    1.22  
    1.23  
    1.24  fun bg_theory (name, parents, files) int =
    1.25 -  (if int then seq ThyInfo.update_thy parents else ();   (*FIXME robust!? *)
    1.26 -    begin_theory name parents files);
    1.27 +  (if int then begin_update_theory else begin_theory) name parents files;
    1.28  
    1.29  fun en_theory thy = (end_theory thy; ());
    1.30  
    1.31 @@ -482,7 +484,7 @@
    1.32  (* context switch *)
    1.33  
    1.34  fun context name =
    1.35 -  Toplevel.init_theory (fn _ => (the (#2 (Context.pass None ThyInfo.update_thy name))))
    1.36 +  Toplevel.init_theory (fn _ => (the (#2 (Context.pass None ThyInfo.quiet_update_thy name))))
    1.37    (K ()) (K ());
    1.38  
    1.39