1.1 --- a/src/Pure/Thy/thy_info.ML	Tue Jul 21 20:37:32 2009 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Jul 21 20:37:32 2009 +0200
     1.3 @@ -23,6 +23,7 @@
     1.4    val get_parents: string -> string list
     1.5    val touch_thy: string -> unit
     1.6    val touch_child_thys: string -> unit
     1.7 +  val thy_ord: theory * theory -> order
     1.8    val remove_thy: string -> unit
     1.9    val kill_thy: string -> unit
    1.10    val provide_file: Path.T -> string -> unit
    1.11 @@ -33,7 +34,6 @@
    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 -> unit
    1.18    val register_thy: string -> unit
    1.19 @@ -231,17 +231,36 @@
    1.20  end;
    1.21  
    1.22  
    1.23 -(* manage pending proofs *)
    1.24 +(* management data *)
    1.25 +
    1.26 +structure Management_Data = TheoryDataFun
    1.27 +(
    1.28 +  type T =
    1.29 +    Task_Queue.group option *   (*worker thread group*)
    1.30 +    int;                        (*abstract update time*)
    1.31 +  val empty = (NONE, 0);
    1.32 +  val copy = I;
    1.33 +  fun extend _ = empty;
    1.34 +  fun merge _ _ = empty;
    1.35 +);
    1.36 +
    1.37 +val thy_ord = int_ord o pairself (#2 o Management_Data.get);
    1.38 +
    1.39 +
    1.40 +(* pending proofs *)
    1.41  
    1.42  fun join_thy name =
    1.43    (case lookup_theory name of
    1.44 -    NONE => []
    1.45 +    NONE => ()
    1.46    | SOME thy => PureThy.join_proofs thy);
    1.47  
    1.48  fun cancel_thy name =
    1.49    (case lookup_theory name of
    1.50      NONE => ()
    1.51 -  | SOME thy => PureThy.cancel_proofs thy);
    1.52 +  | SOME thy =>
    1.53 +      (case #1 (Management_Data.get thy) of
    1.54 +        NONE => ()
    1.55 +      | SOME group => Future.cancel_group group));
    1.56  
    1.57  
    1.58  (* remove theory *)
    1.59 @@ -374,8 +393,7 @@
    1.60      val exns = tasks |> maps (fn (name, _) =>
    1.61        let
    1.62          val after_load = Future.join (the (Symtab.lookup futures name));
    1.63 -        val proof_exns = join_thy name;
    1.64 -        val _ = null proof_exns orelse raise Exn.EXCEPTIONS proof_exns;
    1.65 +        val _ = join_thy name;
    1.66          val _ = after_load ();
    1.67        in [] end handle exn => (kill_thy name; [exn]));
    1.68  
    1.69 @@ -509,20 +527,6 @@
    1.70  end;
    1.71  
    1.72  
    1.73 -(* update_time *)
    1.74 -
    1.75 -structure UpdateTime = TheoryDataFun
    1.76 -(
    1.77 -  type T = int;
    1.78 -  val empty = 0;
    1.79 -  val copy = I;
    1.80 -  fun extend _ = empty;
    1.81 -  fun merge _ _ = empty;
    1.82 -);
    1.83 -
    1.84 -val thy_ord = int_ord o pairself UpdateTime.get;
    1.85 -
    1.86 -
    1.87  (* begin / end theory *)
    1.88  
    1.89  fun begin_theory name parents uses int =
    1.90 @@ -542,7 +546,7 @@
    1.91      val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
    1.92      val update_time = if update_time > 0 then update_time else serial ();
    1.93      val theory' = theory
    1.94 -      |> UpdateTime.put update_time
    1.95 +      |> Management_Data.put (Future.worker_group (), update_time)
    1.96        |> Present.begin_theory update_time dir uses;
    1.97  
    1.98      val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
    1.99 @@ -569,7 +573,7 @@
   1.100      val _ = check_unfinished error name;
   1.101      val _ = touch_thy name;
   1.102      val master = #master (ThyLoad.deps_thy Path.current name);
   1.103 -    val upd_time = UpdateTime.get thy;
   1.104 +    val upd_time = #2 (Management_Data.get thy);
   1.105    in
   1.106      CRITICAL (fn () =>
   1.107       (change_deps name (Option.map