Thy_Load.check_loaded via Theory.at_end;
authorwenzelm
Sun Jul 25 12:57:29 2010 +0200 (2010-07-25 ago)
changeset 37952f6c40213675b
parent 37951 4e2aaf080572
child 37953 ddc3b72f9a42
Thy_Load.check_loaded via Theory.at_end;
src/Pure/Isar/isar_cmd.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Jul 24 21:40:48 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Jul 25 12:57:29 2010 +0200
     1.3 @@ -276,7 +276,7 @@
     1.4  fun init_theory (name, imports, uses) =
     1.5    Toplevel.init_theory name
     1.6      (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses))
     1.7 -    (Theory.end_theory #> tap Thy_Load.check_loaded #> Thy_Info.end_theory);
     1.8 +    (Theory.end_theory #> Thy_Info.end_theory);
     1.9  
    1.10  val exit = Toplevel.keep (fn state =>
    1.11   (Context.set_thread_data (try Toplevel.generic_theory_of state);
     2.1 --- a/src/Pure/Thy/thy_load.ML	Sat Jul 24 21:40:48 2010 +0200
     2.2 +++ b/src/Pure/Thy/thy_load.ML	Sun Jul 25 12:57:29 2010 +0200
     2.3 @@ -27,7 +27,6 @@
     2.4    val deps_thy: Path.T -> string ->
     2.5     {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
     2.6    val loaded_files: theory -> Path.T list
     2.7 -  val check_loaded: theory -> unit
     2.8    val all_current: theory -> bool
     2.9    val provide_file: Path.T -> theory -> theory
    2.10    val use_ml: Path.T -> unit
    2.11 @@ -178,6 +177,8 @@
    2.12        | SOME path_info' => eq_snd (op =) (path_info, path_info'));
    2.13    in can check_loaded thy andalso forall current provided end;
    2.14  
    2.15 +val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));
    2.16 +
    2.17  
    2.18  (* provide files *)
    2.19