1.1 --- a/src/Pure/Thy/thy_info.ML	Sat Sep 08 19:58:38 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Sep 08 19:58:39 2007 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4    val lookup_theory: string -> theory option
     1.5    val get_theory: string -> theory
     1.6    val the_theory: string -> theory -> theory
     1.7 +  val is_finished: string -> bool
     1.8    val loaded_files: string -> Path.T list
     1.9    val get_parents: string -> string list
    1.10    val pretty_theory: theory -> Pretty.T
    1.11 @@ -36,6 +37,7 @@
    1.12    val use_thys: string list -> unit
    1.13    val use_thy: string -> unit
    1.14    val time_use_thy: string -> unit
    1.15 +  val thy_ord: theory * theory -> order
    1.16    val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
    1.17    val end_theory: theory -> theory
    1.18    val register_thy: string -> unit
    1.19 @@ -165,7 +167,7 @@
    1.20      error (loader_msg "nothing known about theory" [name]);
    1.21  
    1.22  
    1.23 -(* pretty printing a theory *)
    1.24 +(* pretty_theory *)
    1.25  
    1.26  local
    1.27  
    1.28 @@ -486,6 +488,20 @@
    1.29      end;
    1.30  
    1.31  
    1.32 +(* update_time *)
    1.33 +
    1.34 +structure UpdateTime = TheoryDataFun
    1.35 +(
    1.36 +  type T = int;
    1.37 +  val empty = 0;
    1.38 +  val copy = I;
    1.39 +  fun extend _ = empty;
    1.40 +  fun merge _ _ = empty;
    1.41 +);
    1.42 +
    1.43 +val thy_ord = int_ord o pairself UpdateTime.get;
    1.44 +
    1.45 +
    1.46  (* begin / end theory *)
    1.47  
    1.48  fun begin_theory name parents uses int =
    1.49 @@ -506,7 +522,10 @@
    1.50      val _ = change_thys (new_deps name parent_names (deps, NONE));
    1.51  
    1.52      val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
    1.53 -    val theory' = Present.begin_theory update_time dir uses theory;
    1.54 +    val update_time = if update_time > 0 then update_time else serial ();
    1.55 +    val theory' = theory
    1.56 +      |> UpdateTime.put update_time
    1.57 +      |> Present.begin_theory update_time dir uses;
    1.58  
    1.59      val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
    1.60      val ((), theory'') =
    1.61 @@ -528,12 +547,12 @@
    1.62  fun register_thy name =
    1.63    let
    1.64      val _ = priority ("Registering theory " ^ quote name);
    1.65 -    val _ = get_theory name;
    1.66 +    val thy = get_theory name;
    1.67      val _ = map get_theory (get_parents name);
    1.68      val _ = check_unfinished error name;
    1.69      val _ = touch_thy name;
    1.70      val master = #master (ThyLoad.deps_thy Path.current name);
    1.71 -    val upd_time = serial ();
    1.72 +    val upd_time = UpdateTime.get thy;
    1.73    in
    1.74      CRITICAL (fn () =>
    1.75       (change_deps name (Option.map