merged
authorwenzelm
Sun Aug 21 13:36:23 2011 +0200 (2011-08-21)
changeset 44351b7f9e764532a
parent 44350 63cddfbc5a09
parent 44341 a93d25fb14fc
child 44352 176e0fb6906b
merged
     1.1 --- a/Admin/polyml/future/ROOT.ML	Sat Aug 20 15:19:35 2011 -0700
     1.2 +++ b/Admin/polyml/future/ROOT.ML	Sun Aug 21 13:36:23 2011 +0200
     1.3 @@ -78,7 +78,6 @@
     1.4  use "General/table.ML";
     1.5  use "General/graph.ML";
     1.6  use "General/ord_list.ML";
     1.7 -use "General/balanced_tree.ML";
     1.8  
     1.9  structure Position =
    1.10  struct
     2.1 --- a/src/HOL/Library/Multiset.thy	Sat Aug 20 15:19:35 2011 -0700
     2.2 +++ b/src/HOL/Library/Multiset.thy	Sun Aug 21 13:36:23 2011 +0200
     2.3 @@ -1598,7 +1598,7 @@
     2.4  definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
     2.5    "image_mset f = fold_mset (op + o single o f) {#}"
     2.6  
     2.7 -interpretation image_fun_commute: comp_fun_commute "op + o single o f"
     2.8 +interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f
     2.9  proof qed (simp add: add_ac fun_eq_iff)
    2.10  
    2.11  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
     3.1 --- a/src/HOL/Tools/Function/context_tree.ML	Sat Aug 20 15:19:35 2011 -0700
     3.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Sun Aug 21 13:36:23 2011 +0200
     3.3 @@ -205,7 +205,7 @@
     3.4          SOME _ => (T, x)
     3.5        | NONE =>
     3.6          let
     3.7 -          val (T', x') = fold fill_table (Int_Graph.imm_succs G i) (T, x)
     3.8 +          val (T', x') = Int_Graph.Keys.fold fill_table (Int_Graph.imm_succs G i) (T, x)
     3.9            val (v, x'') = f (the o Inttab.lookup T') i x'
    3.10          in
    3.11            (Inttab.update (i, v) T', x'')
    3.12 @@ -226,7 +226,7 @@
    3.13              fun sub_step lu i x =
    3.14                let
    3.15                  val (ctxt', subtree) = nth branches i
    3.16 -                val used = fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
    3.17 +                val used = Int_Graph.Keys.fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
    3.18                  val (subs, x') = traverse_help (compose ctxt ctxt') subtree used x
    3.19                  val exported_subs = map (apfst (compose ctxt')) subs (* FIXME: Right order of composition? *)
    3.20                in
    3.21 @@ -264,7 +264,7 @@
    3.22            fun sub_step lu i x =
    3.23              let
    3.24                val ((fixes, assumes), st) = nth branches i
    3.25 -              val used = map lu (Int_Graph.imm_succs deps i)
    3.26 +              val used = map lu (Int_Graph.immediate_succs deps i)
    3.27                  |> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
    3.28                  |> filter_out Thm.is_reflexive
    3.29  
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Aug 20 15:19:35 2011 -0700
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sun Aug 21 13:36:23 2011 +0200
     4.3 @@ -303,7 +303,7 @@
     4.4      val mapping = Termtab.empty |> fold (fn consts => fold (fn const =>
     4.5        Termtab.update (const, consts)) consts) constss;
     4.6      fun succs consts = consts
     4.7 -      |> maps (Term_Graph.imm_succs gr)
     4.8 +      |> maps (Term_Graph.immediate_succs gr)
     4.9        |> subtract eq_cname consts
    4.10        |> map (the o Termtab.lookup mapping)
    4.11        |> distinct (eq_list eq_cname);
     5.1 --- a/src/Pure/Concurrent/future.ML	Sat Aug 20 15:19:35 2011 -0700
     5.2 +++ b/src/Pure/Concurrent/future.ML	Sun Aug 21 13:36:23 2011 +0200
     5.3 @@ -62,12 +62,13 @@
     5.4    val fork: (unit -> 'a) -> 'a future
     5.5    val join_results: 'a future list -> 'a Exn.result list
     5.6    val join_result: 'a future -> 'a Exn.result
     5.7 +  val joins: 'a future list -> 'a list
     5.8    val join: 'a future -> 'a
     5.9    val join_tasks: task list -> unit
    5.10    val value_result: 'a Exn.result -> 'a future
    5.11    val value: 'a -> 'a future
    5.12 +  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
    5.13    val map: ('a -> 'b) -> 'a future -> 'b future
    5.14 -  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
    5.15    val promise_group: group -> (unit -> unit) -> 'a future
    5.16    val promise: (unit -> unit) -> 'a future
    5.17    val fulfill_result: 'a future -> 'a Exn.result -> unit
    5.18 @@ -185,13 +186,21 @@
    5.19  (* cancellation primitives *)
    5.20  
    5.21  fun cancel_now group = (*requires SYNCHRONIZED*)
    5.22 -  Task_Queue.cancel (! queue) group;
    5.23 +  let
    5.24 +    val (tasks, threads) = Task_Queue.cancel (! queue) group;
    5.25 +    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
    5.26 +  in tasks end;
    5.27 +
    5.28 +fun cancel_all () = (*requires SYNCHRONIZED*)
    5.29 +  let
    5.30 +    val (groups, threads) = Task_Queue.cancel_all (! queue);
    5.31 +    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
    5.32 +  in groups end;
    5.33  
    5.34  fun cancel_later group = (*requires SYNCHRONIZED*)
    5.35   (Unsynchronized.change canceled (insert Task_Queue.eq_group group);
    5.36    broadcast scheduler_event);
    5.37  
    5.38 -
    5.39  fun interruptible_task f x =
    5.40    (if Multithreading.available then
    5.41      Multithreading.with_attributes
    5.42 @@ -379,7 +388,7 @@
    5.43    handle exn =>
    5.44      if Exn.is_interrupt exn then
    5.45       (Multithreading.tracing 1 (fn () => "Interrupt");
    5.46 -      List.app cancel_later (Task_Queue.cancel_all (! queue));
    5.47 +      List.app cancel_later (cancel_all ());
    5.48        broadcast_work (); true)
    5.49      else reraise exn;
    5.50  
    5.51 @@ -534,6 +543,7 @@
    5.52  end;
    5.53  
    5.54  fun join_result x = singleton join_results x;
    5.55 +fun joins xs = Par_Exn.release_all (join_results xs);
    5.56  fun join x = Exn.release (join_result x);
    5.57  
    5.58  fun join_tasks [] = ()
    5.59 @@ -556,6 +566,10 @@
    5.60  
    5.61  fun value x = value_result (Exn.Res x);
    5.62  
    5.63 +fun cond_forks args es =
    5.64 +  if Multithreading.enabled () then forks args es
    5.65 +  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
    5.66 +
    5.67  fun map_future f x =
    5.68    let
    5.69      val task = task_of x;
    5.70 @@ -569,16 +583,12 @@
    5.71    in
    5.72      if extended then Future {promised = false, task = task, result = result}
    5.73      else
    5.74 -      (singleton o forks)
    5.75 +      (singleton o cond_forks)
    5.76          {name = "map_future", group = SOME group, deps = [task],
    5.77            pri = Task_Queue.pri_of_task task, interrupts = true}
    5.78          (fn () => f (join x))
    5.79    end;
    5.80  
    5.81 -fun cond_forks args es =
    5.82 -  if Multithreading.enabled () then forks args es
    5.83 -  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
    5.84 -
    5.85  
    5.86  (* promised futures -- fulfilled by external means *)
    5.87  
     6.1 --- a/src/Pure/Concurrent/par_exn.ML	Sat Aug 20 15:19:35 2011 -0700
     6.2 +++ b/src/Pure/Concurrent/par_exn.ML	Sun Aug 21 13:36:23 2011 +0200
     6.3 @@ -43,7 +43,7 @@
     6.4    | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
     6.5  
     6.6  fun make exns =
     6.7 -  (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of
     6.8 +  (case Ord_List.unions exn_ord (map par_exns exns) of
     6.9      [] => Exn.Interrupt
    6.10    | es => Par_Exn es);
    6.11  
     7.1 --- a/src/Pure/Concurrent/task_queue.ML	Sat Aug 20 15:19:35 2011 -0700
     7.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sun Aug 21 13:36:23 2011 +0200
     7.3 @@ -31,8 +31,8 @@
     7.4    val known_task: queue -> task -> bool
     7.5    val all_passive: queue -> bool
     7.6    val status: queue -> {ready: int, pending: int, running: int, passive: int}
     7.7 -  val cancel: queue -> group -> task list
     7.8 -  val cancel_all: queue -> group list
     7.9 +  val cancel: queue -> group -> task list * Thread.thread list
    7.10 +  val cancel_all: queue -> group list * Thread.thread list
    7.11    val finish: task -> queue -> bool * queue
    7.12    val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
    7.13    val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
    7.14 @@ -211,9 +211,11 @@
    7.15  
    7.16  (* job status *)
    7.17  
    7.18 -fun ready_job task (Job list, ([], _)) = SOME (task, rev list)
    7.19 -  | ready_job task (Passive abort, ([], _)) =
    7.20 -      if is_canceled (group_of_task task) then SOME (task, [fn _ => abort ()])
    7.21 +fun ready_job task (Job list, (deps, _)) =
    7.22 +      if Task_Graph.Keys.is_empty deps then SOME (task, rev list) else NONE
    7.23 +  | ready_job task (Passive abort, (deps, _)) =
    7.24 +      if Task_Graph.Keys.is_empty deps andalso is_canceled (group_of_task task)
    7.25 +      then SOME (task, [fn _ => abort ()])
    7.26        else NONE
    7.27    | ready_job _ _ = NONE;
    7.28  
    7.29 @@ -232,7 +234,7 @@
    7.30      val (x, y, z, w) =
    7.31        Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
    7.32            (case job of
    7.33 -            Job _ => if null deps then (x + 1, y, z, w) else (x, y + 1, z, w)
    7.34 +            Job _ => if Task_Graph.Keys.is_empty deps then (x + 1, y, z, w) else (x, y + 1, z, w)
    7.35            | Running _ => (x, y, z + 1, w)
    7.36            | Passive _ => (x, y, z, w + 1)))
    7.37          jobs (0, 0, 0, 0);
    7.38 @@ -248,12 +250,13 @@
    7.39    let
    7.40      val _ = cancel_group group Exn.Interrupt;
    7.41      val running =
    7.42 -      Tasks.fold (fn (task, _) =>
    7.43 -          (case get_job jobs task of Running thread => cons (task, thread) | _ => I))
    7.44 -        (get_tasks groups (group_id group)) [];
    7.45 -    val threads = fold (insert Thread.equal o #2) running [];
    7.46 -    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
    7.47 -  in map #1 running end;
    7.48 +      Tasks.fold (fn (task, _) => fn (tasks, threads) =>
    7.49 +          (case get_job jobs task of
    7.50 +            Running thread => (task :: tasks, insert Thread.equal thread threads)
    7.51 +          | Passive _ => (task :: tasks, threads)
    7.52 +          | _ => (tasks, threads)))
    7.53 +        (get_tasks groups (group_id group)) ([], []);
    7.54 +  in running end;
    7.55  
    7.56  fun cancel_all (Queue {jobs, ...}) =
    7.57    let
    7.58 @@ -266,9 +269,8 @@
    7.59            Running t => (insert eq_group group groups, insert Thread.equal t running)
    7.60          | _ => (groups, running))
    7.61        end;
    7.62 -    val (running_groups, running) = Task_Graph.fold cancel_job jobs ([], []);
    7.63 -    val _ = List.app Simple_Thread.interrupt_unsynchronized running;
    7.64 -  in running_groups end;
    7.65 +    val running = Task_Graph.fold cancel_job jobs ([], []);
    7.66 +  in running end;
    7.67  
    7.68  
    7.69  (* finish *)
    7.70 @@ -278,7 +280,7 @@
    7.71      val group = group_of_task task;
    7.72      val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups;
    7.73      val jobs' = Task_Graph.del_node task jobs;
    7.74 -    val maximal = null (Task_Graph.imm_succs jobs task);
    7.75 +    val maximal = Task_Graph.is_maximal jobs task;
    7.76    in (maximal, make_queue groups' jobs') end;
    7.77  
    7.78  
    7.79 @@ -342,7 +344,7 @@
    7.80            else
    7.81              let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in
    7.82                (case ready_job task entry of
    7.83 -                NONE => ready_dep (Tasks.update (task, ()) seen) (ds @ tasks)
    7.84 +                NONE => ready_dep (Tasks.update (task, ()) seen) (Task_Graph.Keys.dest ds @ tasks)
    7.85                | some => some)
    7.86              end;
    7.87  
     8.1 --- a/src/Pure/General/graph.ML	Sat Aug 20 15:19:35 2011 -0700
     8.2 +++ b/src/Pure/General/graph.ML	Sun Aug 21 13:36:23 2011 +0200
     8.3 @@ -7,6 +7,14 @@
     8.4  signature GRAPH =
     8.5  sig
     8.6    type key
     8.7 +  structure Keys:
     8.8 +  sig
     8.9 +    type T
    8.10 +    val is_empty: T -> bool
    8.11 +    val fold: (key -> 'a -> 'a) -> T -> 'a -> 'a
    8.12 +    val fold_rev: (key -> 'a -> 'a) -> T -> 'a -> 'a
    8.13 +    val dest: T -> key list
    8.14 +  end
    8.15    type 'a T
    8.16    exception DUP of key
    8.17    exception SAME
    8.18 @@ -15,20 +23,24 @@
    8.19    val is_empty: 'a T -> bool
    8.20    val keys: 'a T -> key list
    8.21    val dest: 'a T -> (key * key list) list
    8.22 -  val get_first: (key * ('a * (key list * key list)) -> 'b option) -> 'a T -> 'b option
    8.23 -  val fold: (key * ('a * (key list * key list)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
    8.24 -  val minimals: 'a T -> key list
    8.25 -  val maximals: 'a T -> key list
    8.26 +  val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
    8.27 +  val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
    8.28    val subgraph: (key -> bool) -> 'a T -> 'a T
    8.29 -  val get_entry: 'a T -> key -> key * ('a * (key list * key list))    (*exception UNDEF*)
    8.30 +  val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
    8.31    val map: (key -> 'a -> 'b) -> 'a T -> 'b T
    8.32    val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
    8.33    val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
    8.34    val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
    8.35 -  val imm_preds: 'a T -> key -> key list
    8.36 -  val imm_succs: 'a T -> key -> key list
    8.37 +  val imm_preds: 'a T -> key -> Keys.T
    8.38 +  val imm_succs: 'a T -> key -> Keys.T
    8.39 +  val immediate_preds: 'a T -> key -> key list
    8.40 +  val immediate_succs: 'a T -> key -> key list
    8.41    val all_preds: 'a T -> key list -> key list
    8.42    val all_succs: 'a T -> key list -> key list
    8.43 +  val minimals: 'a T -> key list
    8.44 +  val maximals: 'a T -> key list
    8.45 +  val is_minimal: 'a T -> key -> bool
    8.46 +  val is_maximal: 'a T -> key -> bool
    8.47    val strong_conn: 'a T -> key list list
    8.48    val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
    8.49    val default_node: key * 'a -> 'a T -> 'a T
    8.50 @@ -59,27 +71,38 @@
    8.51  (* keys *)
    8.52  
    8.53  type key = Key.key;
    8.54 -
    8.55  val eq_key = is_equal o Key.ord;
    8.56  
    8.57 -val member_key = member eq_key;
    8.58 -val remove_key = remove eq_key;
    8.59 +structure Table = Table(Key);
    8.60 +
    8.61 +structure Keys =
    8.62 +struct
    8.63  
    8.64 +abstype T = Keys of unit Table.table
    8.65 +with
    8.66  
    8.67 -(* tables and sets of keys *)
    8.68 +val empty = Keys Table.empty;
    8.69 +fun is_empty (Keys tab) = Table.is_empty tab;
    8.70  
    8.71 -structure Table = Table(Key);
    8.72 -type keys = unit Table.table;
    8.73 +fun member (Keys tab) = Table.defined tab;
    8.74 +fun insert x (Keys tab) = Keys (Table.insert (K true) (x, ()) tab);
    8.75 +fun remove x (Keys tab) = Keys (Table.delete_safe x tab);
    8.76 +
    8.77 +fun fold f (Keys tab) = Table.fold (f o #1) tab;
    8.78 +fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab;
    8.79  
    8.80 -val empty_keys = Table.empty: keys;
    8.81 +fun make xs = Basics.fold insert xs empty;
    8.82 +fun dest keys = fold_rev cons keys [];
    8.83  
    8.84 -fun member_keys tab = Table.defined (tab: keys);
    8.85 -fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
    8.86 +fun filter P keys = fold (fn x => P x ? insert x) keys empty;
    8.87 +
    8.88 +end;
    8.89 +end;
    8.90  
    8.91  
    8.92  (* graphs *)
    8.93  
    8.94 -datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
    8.95 +datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table;
    8.96  
    8.97  exception DUP = Table.DUP;
    8.98  exception UNDEF = Table.UNDEF;
    8.99 @@ -88,18 +111,16 @@
   8.100  val empty = Graph Table.empty;
   8.101  fun is_empty (Graph tab) = Table.is_empty tab;
   8.102  fun keys (Graph tab) = Table.keys tab;
   8.103 -fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
   8.104 +fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab);
   8.105  
   8.106  fun get_first f (Graph tab) = Table.get_first f tab;
   8.107  fun fold_graph f (Graph tab) = Table.fold f tab;
   8.108  
   8.109 -fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G [];
   8.110 -fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m | _ => I) G [];
   8.111 -
   8.112  fun subgraph P G =
   8.113    let
   8.114      fun subg (k, (i, (preds, succs))) =
   8.115 -      if P k then Table.update (k, (i, (filter P preds, filter P succs))) else I;
   8.116 +      if P k then Table.update (k, (i, (Keys.filter P preds, Keys.filter P succs)))
   8.117 +      else I;
   8.118    in Graph (fold_graph subg G Table.empty) end;
   8.119  
   8.120  fun get_entry (Graph tab) x =
   8.121 @@ -132,20 +153,29 @@
   8.122  fun reachable next xs =
   8.123    let
   8.124      fun reach x (rs, R) =
   8.125 -      if member_keys R x then (rs, R)
   8.126 -      else fold reach (next x) (rs, insert_keys x R) |>> cons x;
   8.127 +      if Keys.member R x then (rs, R)
   8.128 +      else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x;
   8.129      fun reachs x (rss, R) =
   8.130        reach x ([], R) |>> (fn rs => rs :: rss);
   8.131 -  in fold reachs xs ([], empty_keys) end;
   8.132 +  in fold reachs xs ([], Keys.empty) end;
   8.133  
   8.134  (*immediate*)
   8.135  fun imm_preds G = #1 o #2 o #2 o get_entry G;
   8.136  fun imm_succs G = #2 o #2 o #2 o get_entry G;
   8.137  
   8.138 +fun immediate_preds G = Keys.dest o imm_preds G;
   8.139 +fun immediate_succs G = Keys.dest o imm_succs G;
   8.140 +
   8.141  (*transitive*)
   8.142  fun all_preds G = flat o #1 o reachable (imm_preds G);
   8.143  fun all_succs G = flat o #1 o reachable (imm_succs G);
   8.144  
   8.145 +(*minimal and maximal elements*)
   8.146 +fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G [];
   8.147 +fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G [];
   8.148 +fun is_minimal G x = Keys.is_empty (imm_preds G x);
   8.149 +fun is_maximal G x = Keys.is_empty (imm_succs G x);
   8.150 +
   8.151  (*strongly connected components; see: David King and John Launchbury,
   8.152    "Structuring Depth First Search Algorithms in Haskell"*)
   8.153  fun strong_conn G =
   8.154 @@ -155,43 +185,44 @@
   8.155  (* nodes *)
   8.156  
   8.157  fun new_node (x, info) (Graph tab) =
   8.158 -  Graph (Table.update_new (x, (info, ([], []))) tab);
   8.159 +  Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
   8.160  
   8.161  fun default_node (x, info) (Graph tab) =
   8.162 -  Graph (Table.default (x, (info, ([], []))) tab);
   8.163 +  Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);
   8.164  
   8.165  fun del_nodes xs (Graph tab) =
   8.166    Graph (tab
   8.167      |> fold Table.delete xs
   8.168      |> Table.map (fn _ => fn (i, (preds, succs)) =>
   8.169 -      (i, (fold remove_key xs preds, fold remove_key xs succs))));
   8.170 +      (i, (fold Keys.remove xs preds, fold Keys.remove xs succs))));
   8.171  
   8.172  fun del_node x (G as Graph tab) =
   8.173    let
   8.174 -    fun del_adjacent which y = Table.map_entry y (fn (i, ps) => (i, (which (remove_key x) ps)));
   8.175 +    fun del_adjacent which y =
   8.176 +      Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove x) ps)));
   8.177      val (preds, succs) = #2 (#2 (get_entry G x));
   8.178    in
   8.179      Graph (tab
   8.180        |> Table.delete x
   8.181 -      |> fold (del_adjacent apsnd) preds
   8.182 -      |> fold (del_adjacent apfst) succs)
   8.183 +      |> Keys.fold (del_adjacent apsnd) preds
   8.184 +      |> Keys.fold (del_adjacent apfst) succs)
   8.185    end;
   8.186  
   8.187  
   8.188  (* edges *)
   8.189  
   8.190 -fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
   8.191 +fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;
   8.192  
   8.193  fun add_edge (x, y) G =
   8.194    if is_edge G (x, y) then G
   8.195    else
   8.196 -    G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))
   8.197 -      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y :: succs)));
   8.198 +    G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.insert x preds, succs)))
   8.199 +      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.insert y succs)));
   8.200  
   8.201  fun del_edge (x, y) G =
   8.202    if is_edge G (x, y) then
   8.203 -    G |> map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs)))
   8.204 -      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, remove_key y succs)))
   8.205 +    G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs)))
   8.206 +      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs)))
   8.207    else G;
   8.208  
   8.209  fun diff_edges G1 G2 =
   8.210 @@ -203,7 +234,7 @@
   8.211  
   8.212  (* join and merge *)
   8.213  
   8.214 -fun no_edges (i, _) = (i, ([], []));
   8.215 +fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));
   8.216  
   8.217  fun join f (G1 as Graph tab1, G2 as Graph tab2) =
   8.218    let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in
   8.219 @@ -227,11 +258,11 @@
   8.220      fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z));
   8.221      fun irreds [] xs' = xs'
   8.222        | irreds (x :: xs) xs' =
   8.223 -          if not (member_keys X x) orelse eq_key (x, z) orelse member_key path x orelse
   8.224 +          if not (Keys.member X x) orelse eq_key (x, z) orelse member eq_key path x orelse
   8.225              exists (red x) xs orelse exists (red x) xs'
   8.226            then irreds xs xs'
   8.227            else irreds xs (x :: xs');
   8.228 -  in irreds (imm_preds G z) [] end;
   8.229 +  in irreds (immediate_preds G z) [] end;
   8.230  
   8.231  fun irreducible_paths G (x, y) =
   8.232    let
   8.233 @@ -249,8 +280,8 @@
   8.234      val (_, X) = reachable (imm_succs G) [x];
   8.235      fun paths path z =
   8.236        if not (null path) andalso eq_key (x, z) then [z :: path]
   8.237 -      else if member_keys X z andalso not (member_key path z)
   8.238 -      then maps (paths (z :: path)) (imm_preds G z)
   8.239 +      else if Keys.member X z andalso not (member eq_key path z)
   8.240 +      then maps (paths (z :: path)) (immediate_preds G z)
   8.241        else [];
   8.242    in paths [] y end;
   8.243  
   8.244 @@ -297,7 +328,7 @@
   8.245      val results = (xs, Table.empty) |-> fold (fn x => fn tab =>
   8.246        let
   8.247          val a = get_node G x;
   8.248 -        val deps = imm_preds G x |> map (fn y =>
   8.249 +        val deps = immediate_preds G x |> map (fn y =>
   8.250            (case Table.lookup tab y of
   8.251              SOME b => (y, b)
   8.252            | NONE => raise DEP (x, y)));
     9.1 --- a/src/Pure/General/ord_list.ML	Sat Aug 20 15:19:35 2011 -0700
     9.2 +++ b/src/Pure/General/ord_list.ML	Sun Aug 21 13:36:23 2011 +0200
     9.3 @@ -14,6 +14,7 @@
     9.4    val remove: ('b * 'a -> order) -> 'b -> 'a T -> 'a T
     9.5    val subset: ('b * 'a -> order) -> 'b T * 'a T -> bool
     9.6    val union: ('a * 'a -> order) -> 'a T -> 'a T -> 'a T
     9.7 +  val unions: ('a * 'a -> order) -> 'a T list -> 'a T
     9.8    val merge: ('a * 'a -> order) -> 'a T * 'a T -> 'a T
     9.9    val inter: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
    9.10    val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
    9.11 @@ -86,6 +87,15 @@
    9.12            | GREATER => y :: unio lst1 ys);
    9.13    in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
    9.14  
    9.15 +fun unions ord lists =
    9.16 +  let
    9.17 +    fun unios (xs :: ys :: rest) acc = unios rest (union ord xs ys :: acc)
    9.18 +      | unios [xs] (ys :: acc) = unios (union ord xs ys :: acc) []
    9.19 +      | unios [xs] [] = xs
    9.20 +      | unios [] [] = []
    9.21 +      | unios [] acc = unios acc [];
    9.22 +  in unios lists [] end;
    9.23 +
    9.24  fun merge ord (list1, list2) = union ord list2 list1;
    9.25  
    9.26  (*intersection: filter second list for elements present in first list*)
    10.1 --- a/src/Pure/General/table.ML	Sat Aug 20 15:19:35 2011 -0700
    10.2 +++ b/src/Pure/General/table.ML	Sun Aug 21 13:36:23 2011 +0200
    10.3 @@ -340,7 +340,7 @@
    10.4  in
    10.5  
    10.6  fun delete key tab = snd (snd (del (SOME key) tab));
    10.7 -fun delete_safe key tab = delete key tab handle UNDEF _ => tab;
    10.8 +fun delete_safe key tab = if defined tab key then delete key tab else tab;
    10.9  
   10.10  end;
   10.11  
    11.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Aug 20 15:19:35 2011 -0700
    11.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Aug 21 13:36:23 2011 +0200
    11.3 @@ -407,7 +407,7 @@
    11.4      val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
    11.5      val classes = Sorts.classes_of algebra;
    11.6      fun entry (c, (i, (_, cs))) =
    11.7 -      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = cs,
    11.8 +      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
    11.9              dir = "", unfold = true, path = ""});
   11.10      val gr =
   11.11        Graph.fold (cons o entry) classes []
    12.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 20 15:19:35 2011 -0700
    12.2 +++ b/src/Pure/PIDE/document.ML	Sun Aug 21 13:36:23 2011 +0200
    12.3 @@ -145,7 +145,8 @@
    12.4                |> default_node name
    12.5                |> fold default_node parents;
    12.6              val nodes2 = nodes1
    12.7 -              |> fold (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    12.8 +              |> Graph.Keys.fold
    12.9 +                  (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
   12.10              val (header', nodes3) =
   12.11                (header, Graph.add_deps_acyclic (name, parents) nodes2)
   12.12                  handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
   12.13 @@ -371,7 +372,7 @@
   12.14                          |> set_result result;
   12.15                      in ((assigns, execs, [(name, node')]), node') end)
   12.16                end))
   12.17 -      |> Future.join_results |> Par_Exn.release_all |> map #1;
   12.18 +      |> Future.joins |> map #1;
   12.19  
   12.20      val state' = state
   12.21        |> fold (fold define_exec o #2) updates
    13.1 --- a/src/Pure/Thy/thm_deps.ML	Sat Aug 20 15:19:35 2011 -0700
    13.2 +++ b/src/Pure/Thy/thm_deps.ML	Sun Aug 21 13:36:23 2011 +0200
    13.3 @@ -40,7 +40,7 @@
    13.4                 path = "",
    13.5                 parents = parents};
    13.6            in cons entry end;
    13.7 -    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
    13.8 +    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
    13.9    in Present.display_graph (sort_wrt #ID deps) end;
   13.10  
   13.11  
   13.12 @@ -66,7 +66,8 @@
   13.13      val used =
   13.14        Proofterm.fold_body_thms
   13.15          (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
   13.16 -        (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) new_thms) Symtab.empty;
   13.17 +        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
   13.18 +        Symtab.empty;
   13.19  
   13.20      fun is_unused a = not (Symtab.defined used a);
   13.21  
    14.1 --- a/src/Pure/Thy/thy_info.ML	Sat Aug 20 15:19:35 2011 -0700
    14.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Aug 21 13:36:23 2011 +0200
    14.3 @@ -113,10 +113,6 @@
    14.4  val is_finished = is_none o get_deps;
    14.5  val master_directory = master_dir o get_deps;
    14.6  
    14.7 -fun get_parents name =
    14.8 -  thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>
    14.9 -    error (loader_msg "nothing known about theory" [name]);
   14.10 -
   14.11  
   14.12  (* access theory *)
   14.13  
   14.14 @@ -130,6 +126,8 @@
   14.15      SOME theory => theory
   14.16    | _ => error (loader_msg "undefined theory entry for" [name]));
   14.17  
   14.18 +val get_imports = Thy_Load.imports_of o get_theory;
   14.19 +
   14.20  fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
   14.21    (case get_deps name of
   14.22      NONE => []
   14.23 @@ -242,7 +240,7 @@
   14.24  
   14.25  fun check_deps dir name =
   14.26    (case lookup_deps name of
   14.27 -    SOME NONE => (true, NONE, get_parents name)
   14.28 +    SOME NONE => (true, NONE, get_imports name)
   14.29    | NONE =>
   14.30        let val {master, text, imports, ...} = Thy_Load.check_thy dir name
   14.31        in (false, SOME (make_deps master imports, text), imports) end
    15.1 --- a/src/Pure/axclass.ML	Sat Aug 20 15:19:35 2011 -0700
    15.2 +++ b/src/Pure/axclass.ML	Sun Aug 21 13:36:23 2011 +0200
    15.3 @@ -220,7 +220,9 @@
    15.4        in ((c1_pred, c2_succ), th') end;
    15.5  
    15.6      val new_classrels =
    15.7 -      Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
    15.8 +      Library.map_product pair
    15.9 +        (c1 :: Graph.immediate_preds classes c1)
   15.10 +        (c2 :: Graph.immediate_succs classes c2)
   15.11        |> filter_out ((op =) orf Symreltab.defined classrels)
   15.12        |> map gen_classrel;
   15.13      val needed = not (null new_classrels);
    16.1 --- a/src/Pure/proofterm.ML	Sat Aug 20 15:19:35 2011 -0700
    16.2 +++ b/src/Pure/proofterm.ML	Sun Aug 21 13:36:23 2011 +0200
    16.3 @@ -37,17 +37,17 @@
    16.4  
    16.5    type oracle = string * term
    16.6    type pthm = serial * (string * term * proof_body future)
    16.7 -  val join_body: proof_body -> unit
    16.8    val proof_of: proof_body -> proof
    16.9    val join_proof: proof_body future -> proof
   16.10    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   16.11    val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
   16.12 +  val join_bodies: proof_body list -> unit
   16.13    val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
   16.14  
   16.15    val oracle_ord: oracle * oracle -> order
   16.16    val thm_ord: pthm * pthm -> order
   16.17 -  val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
   16.18 -  val merge_thms: pthm Ord_List.T -> pthm Ord_List.T -> pthm Ord_List.T
   16.19 +  val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
   16.20 +  val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
   16.21    val all_oracles_of: proof_body -> oracle Ord_List.T
   16.22    val approximate_proof_body: proof -> proof_body
   16.23  
   16.24 @@ -171,13 +171,11 @@
   16.25  type oracle = string * term;
   16.26  type pthm = serial * (string * term * proof_body future);
   16.27  
   16.28 -fun join_thm (pthm: pthm) = ignore (Future.join (#3 (#2 pthm)));
   16.29 -fun join_thms thms = (Future.join_results (map (#3 o #2) thms); List.app join_thm thms);
   16.30 -fun join_body (PBody {thms, ...}) = join_thms thms;
   16.31 -
   16.32  fun proof_of (PBody {proof, ...}) = proof;
   16.33  val join_proof = Future.join #> proof_of;
   16.34  
   16.35 +fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
   16.36 +
   16.37  
   16.38  (***** proof atoms *****)
   16.39  
   16.40 @@ -208,6 +206,8 @@
   16.41            in (f (name, prop, body') x', seen') end);
   16.42    in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
   16.43  
   16.44 +fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
   16.45 +
   16.46  fun status_of bodies =
   16.47    let
   16.48      fun status (PBody {oracles, thms, ...}) x =
   16.49 @@ -237,8 +237,8 @@
   16.50  val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
   16.51  fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
   16.52  
   16.53 -val merge_oracles = Ord_List.union oracle_ord;
   16.54 -val merge_thms = Ord_List.union thm_ord;
   16.55 +val unions_oracles = Ord_List.unions oracle_ord;
   16.56 +val unions_thms = Ord_List.unions thm_ord;
   16.57  
   16.58  val all_oracles_of =
   16.59    let
   16.60 @@ -249,8 +249,8 @@
   16.61            let
   16.62              val body' = Future.join body;
   16.63              val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
   16.64 -          in (merge_oracles oracles x', seen') end);
   16.65 -  in fn body => #1 (collect body ([], Inttab.empty)) end;
   16.66 +          in (if null oracles then x' else oracles :: x', seen') end);
   16.67 +  in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;
   16.68  
   16.69  fun approximate_proof_body prf =
   16.70    let
   16.71 @@ -1385,8 +1385,11 @@
   16.72  fun fulfill_norm_proof thy ps body0 =
   16.73    let
   16.74      val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
   16.75 -    val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
   16.76 -    val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
   16.77 +    val oracles =
   16.78 +      unions_oracles
   16.79 +        (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
   16.80 +    val thms =
   16.81 +      unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
   16.82      val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
   16.83  
   16.84      fun fill (Promise (i, prop, Ts)) =
   16.85 @@ -1396,12 +1399,9 @@
   16.86        | fill _ = NONE;
   16.87      val (rules, procs) = get_data thy;
   16.88      val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
   16.89 -    val _ = join_thms thms;
   16.90    in PBody {oracles = oracles, thms = thms, proof = proof} end;
   16.91  
   16.92 -fun fulfill_proof_future _ [] postproc body =
   16.93 -      if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
   16.94 -      else Future.map postproc body
   16.95 +fun fulfill_proof_future _ [] postproc body = Future.map postproc body
   16.96    | fulfill_proof_future thy promises postproc body =
   16.97        (singleton o Future.forks)
   16.98          {name = "Proofterm.fulfill_proof_future", group = NONE,
   16.99 @@ -1460,11 +1460,10 @@
  16.100      fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
  16.101      val body0 =
  16.102        if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
  16.103 -      else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
  16.104        else
  16.105 -        (singleton o Future.forks)
  16.106 +        (singleton o Future.cond_forks)
  16.107            {name = "Proofterm.prepare_thm_proof", group = NONE,
  16.108 -            deps = [], pri = ~1, interrupts = true}
  16.109 +            deps = [], pri = 0, interrupts = true}
  16.110            (make_body0 o full_proof0);
  16.111  
  16.112      fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
    17.1 --- a/src/Pure/sorts.ML	Sat Aug 20 15:19:35 2011 -0700
    17.2 +++ b/src/Pure/sorts.ML	Sun Aug 21 13:36:23 2011 +0200
    17.3 @@ -128,7 +128,7 @@
    17.4  
    17.5  fun all_classes (Algebra {classes, ...}) = Graph.all_preds classes (Graph.maximals classes);
    17.6  
    17.7 -val super_classes = Graph.imm_succs o classes_of;
    17.8 +val super_classes = Graph.immediate_succs o classes_of;
    17.9  
   17.10  
   17.11  (* class relations *)
   17.12 @@ -413,7 +413,7 @@
   17.13        end;
   17.14  
   17.15      fun derive (_, []) = []
   17.16 -      | derive (T as Type (a, Us), S) =
   17.17 +      | derive (Type (a, Us), S) =
   17.18            let
   17.19              val Ss = mg_domain algebra a S;
   17.20              val dom = map2 (fn U => fn S => derive (U, S) ~~ S) Us Ss;
    18.1 --- a/src/Pure/thm.ML	Sat Aug 20 15:19:35 2011 -0700
    18.2 +++ b/src/Pure/thm.ML	Sun Aug 21 13:36:23 2011 +0200
    18.3 @@ -95,9 +95,10 @@
    18.4    val weaken: cterm -> thm -> thm
    18.5    val weaken_sorts: sort list -> cterm -> cterm
    18.6    val extra_shyps: thm -> sort list
    18.7 -  val join_proofs: thm list -> unit
    18.8 +  val proof_bodies_of: thm list -> proof_body list
    18.9    val proof_body_of: thm -> proof_body
   18.10    val proof_of: thm -> proof
   18.11 +  val join_proofs: thm list -> unit
   18.12    val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
   18.13    val future: thm future -> cterm -> thm
   18.14    val derivation_name: thm -> string
   18.15 @@ -491,8 +492,8 @@
   18.16      (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
   18.17    let
   18.18      val ps = Ord_List.union promise_ord ps1 ps2;
   18.19 -    val oras = Proofterm.merge_oracles oras1 oras2;
   18.20 -    val thms = Proofterm.merge_thms thms1 thms2;
   18.21 +    val oras = Proofterm.unions_oracles [oras1, oras2];
   18.22 +    val thms = Proofterm.unions_thms [thms1, thms2];
   18.23      val prf =
   18.24        (case ! Proofterm.proofs of
   18.25          2 => f prf1 prf2
   18.26 @@ -510,18 +511,30 @@
   18.27  
   18.28  (* fulfilled proofs *)
   18.29  
   18.30 -fun raw_body (Thm (Deriv {body, ...}, _)) = body;
   18.31 +fun raw_body_of (Thm (Deriv {body, ...}, _)) = body;
   18.32 +fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises;
   18.33 +
   18.34 +fun join_promises [] = ()
   18.35 +  | join_promises promises = join_promises_of (Future.joins (map snd promises))
   18.36 +and join_promises_of thms = join_promises (maps raw_promises_of thms);
   18.37  
   18.38  fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
   18.39 -  Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
   18.40 -    (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
   18.41 -and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
   18.42 +  Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (fulfill_promises promises) body
   18.43 +and fulfill_promises promises =
   18.44 +  map fst promises ~~ map fulfill_body (Future.joins (map snd promises));
   18.45  
   18.46 -fun join_proofs thms = ignore (map fulfill_body thms);
   18.47 +fun proof_bodies_of thms =
   18.48 +  let
   18.49 +    val _ = join_promises_of thms;
   18.50 +    val bodies = map fulfill_body thms;
   18.51 +    val _ = Proofterm.join_bodies bodies;
   18.52 +  in bodies end;
   18.53  
   18.54 -fun proof_body_of thm = (Proofterm.join_body (raw_body thm); fulfill_body thm);
   18.55 +val proof_body_of = singleton proof_bodies_of;
   18.56  val proof_of = Proofterm.proof_of o proof_body_of;
   18.57  
   18.58 +val join_proofs = ignore o proof_bodies_of;
   18.59 +
   18.60  
   18.61  (* derivation status *)
   18.62  
   18.63 @@ -529,7 +542,7 @@
   18.64    let
   18.65      val ps = map (Future.peek o snd) promises;
   18.66      val bodies = body ::
   18.67 -      map_filter (fn SOME (Exn.Res th) => SOME (raw_body th) | _ => NONE) ps;
   18.68 +      map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps;
   18.69      val {oracle, unfinished, failed} = Proofterm.status_of bodies;
   18.70    in
   18.71     {oracle = oracle,
   18.72 @@ -552,7 +565,7 @@
   18.73      val _ = null hyps orelse err "bad hyps";
   18.74      val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
   18.75      val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
   18.76 -    val _ = fulfill_bodies (map #2 promises);
   18.77 +    val _ = join_promises promises;
   18.78    in thm end;
   18.79  
   18.80  fun future future_thm ct =
    19.1 --- a/src/Tools/Code/code_namespace.ML	Sat Aug 20 15:19:35 2011 -0700
    19.2 +++ b/src/Tools/Code/code_namespace.ML	Sun Aug 21 13:36:23 2011 +0200
    19.3 @@ -86,7 +86,8 @@
    19.4        end;
    19.5      val proto_program = Graph.empty
    19.6        |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
    19.7 -      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
    19.8 +      |> Graph.fold (fn (name, (_, (_, names))) =>
    19.9 +          Graph.Keys.fold (add_dependency name) names) program;
   19.10  
   19.11      (* name declarations and statement modifications *)
   19.12      fun declare name (base, stmt) (gr, nsp) = 
   19.13 @@ -191,7 +192,8 @@
   19.14        in (map_module name_fragments_common o apsnd) add_edge end;
   19.15      val proto_program = empty_program
   19.16        |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
   19.17 -      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
   19.18 +      |> Graph.fold (fn (name, (_, (_, names))) =>
   19.19 +          Graph.Keys.fold (add_dependency name) names) program;
   19.20  
   19.21      (* name declarations, data and statement modifications *)
   19.22      fun make_declarations nsps (data, nodes) =
    20.1 --- a/src/Tools/Code/code_preproc.ML	Sat Aug 20 15:19:35 2011 -0700
    20.2 +++ b/src/Tools/Code/code_preproc.ML	Sun Aug 21 13:36:23 2011 +0200
    20.3 @@ -309,7 +309,7 @@
    20.4      val diff_classes = new_classes |> subtract (op =) old_classes;
    20.5    in if null diff_classes then vardeps_data
    20.6    else let
    20.7 -    val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k;
    20.8 +    val c_ks = Vargraph.immediate_succs (fst vardeps_data) c_k |> insert (op =) c_k;
    20.9    in
   20.10      vardeps_data
   20.11      |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
    21.1 --- a/src/Tools/Code/code_scala.ML	Sat Aug 20 15:19:35 2011 -0700
    21.2 +++ b/src/Tools/Code/code_scala.ML	Sun Aug 21 13:36:23 2011 +0200
    21.3 @@ -321,7 +321,7 @@
    21.4           of Code_Thingol.Classinst _ => true
    21.5            | _ => false;
    21.6          val implicits = filter (is_classinst o Graph.get_node program)
    21.7 -          (Graph.imm_succs program name);
    21.8 +          (Graph.immediate_succs program name);
    21.9        in union (op =) implicits end;
   21.10      fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE
   21.11        | modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
    22.1 --- a/src/Tools/Code/code_thingol.ML	Sat Aug 20 15:19:35 2011 -0700
    22.2 +++ b/src/Tools/Code/code_thingol.ML	Sun Aug 21 13:36:23 2011 +0200
    22.3 @@ -921,7 +921,7 @@
    22.4        let
    22.5          val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
    22.6            Graph.get_node program1 Term.dummy_patternN;
    22.7 -        val deps = Graph.imm_succs program1 Term.dummy_patternN;
    22.8 +        val deps = Graph.immediate_succs program1 Term.dummy_patternN;
    22.9          val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
   22.10          val deps_all = Graph.all_succs program2 deps;
   22.11          val program3 = Graph.subgraph (member (op =) deps_all) program2;
   22.12 @@ -1010,7 +1010,7 @@
   22.13      val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
   22.14        Symtab.update (const, consts)) consts) constss;
   22.15      fun succs consts = consts
   22.16 -      |> maps (Graph.imm_succs eqngr)
   22.17 +      |> maps (Graph.immediate_succs eqngr)
   22.18        |> subtract (op =) consts
   22.19        |> map (the o Symtab.lookup mapping)
   22.20        |> distinct (op =);
    23.1 --- a/src/Tools/codegen.ML	Sat Aug 20 15:19:35 2011 -0700
    23.2 +++ b/src/Tools/codegen.ML	Sun Aug 21 13:36:23 2011 +0200
    23.3 @@ -756,7 +756,7 @@
    23.4            let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
    23.5              if a = a' then Option.map (pair x)
    23.6                (find_first ((fn (_, b', _) => b' = b) o Graph.get_node gr)
    23.7 -                (Graph.imm_succs gr x))
    23.8 +                (Graph.immediate_succs gr x))
    23.9              else NONE) code
   23.10            in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
   23.11        | string_of_cycle _ = ""
   23.12 @@ -767,7 +767,7 @@
   23.13          val mod_gr = fold_rev Graph.add_edge_acyclic
   23.14            (maps (fn (s, (_, module, _)) => map (pair module)
   23.15              (filter_out (fn s => s = module) (map (#2 o Graph.get_node gr)
   23.16 -              (Graph.imm_succs gr s)))) code)
   23.17 +              (Graph.immediate_succs gr s)))) code)
   23.18            (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
   23.19          val modules' =
   23.20            rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
    24.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sat Aug 20 15:19:35 2011 -0700
    24.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Aug 21 13:36:23 2011 +0200
    24.3 @@ -54,19 +54,13 @@
    24.4    session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
    24.5    session_phase.tooltip = "Prover status"
    24.6  
    24.7 -  private val interrupt = new Button("Interrupt") {
    24.8 -    reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
    24.9 -  }
   24.10 -  interrupt.tooltip = "Broadcast interrupt to all prover tasks"
   24.11 -
   24.12    private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
   24.13    logic.listenTo(logic.selection)
   24.14    logic.reactions += {
   24.15      case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
   24.16    }
   24.17  
   24.18 -  private val controls =
   24.19 -    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt, logic)
   24.20 +  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(session_phase, logic)
   24.21    add(controls.peer, BorderLayout.NORTH)
   24.22  
   24.23  
    25.1 --- a/src/Tools/nbe.ML	Sat Aug 20 15:19:35 2011 -0700
    25.2 +++ b/src/Tools/nbe.ML	Sun Aug 21 13:36:23 2011 +0200
    25.3 @@ -471,7 +471,7 @@
    25.4        then (nbe_program, (maxidx, idx_tab))
    25.5        else (nbe_program, (maxidx, idx_tab))
    25.6          |> compile_stmts thy (map (fn name => ((name, Graph.get_node program name),
    25.7 -          Graph.imm_succs program name)) names);
    25.8 +          Graph.immediate_succs program name)) names);
    25.9    in
   25.10      fold_rev add_stmts (Graph.strong_conn program)
   25.11    end;
    26.1 --- a/src/Tools/subtyping.ML	Sat Aug 20 15:19:35 2011 -0700
    26.2 +++ b/src/Tools/subtyping.ML	Sun Aug 21 13:36:23 2011 +0200
    26.3 @@ -171,10 +171,10 @@
    26.4  fun get_succs G T = Typ_Graph.all_succs G [T];
    26.5  fun maybe_new_typnode T G = perhaps (try (Typ_Graph.new_node (T, ()))) G;
    26.6  fun maybe_new_typnodes Ts G = fold maybe_new_typnode Ts G;
    26.7 -fun new_imm_preds G Ts =
    26.8 -  subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.imm_preds G) Ts));
    26.9 -fun new_imm_succs G Ts =
   26.10 -  subtract op= Ts (distinct (op =) (maps (Typ_Graph.imm_succs G) Ts));
   26.11 +fun new_imm_preds G Ts =  (* FIXME inefficient *)
   26.12 +  subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_preds G) Ts));
   26.13 +fun new_imm_succs G Ts =  (* FIXME inefficient *)
   26.14 +  subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_succs G) Ts));
   26.15  
   26.16  
   26.17  (* Graph shortcuts *)
   26.18 @@ -406,7 +406,7 @@
   26.19      (*styps stands either for supertypes or for subtypes of a type T
   26.20        in terms of the subtype-relation (excluding T itself)*)
   26.21      fun styps super T =
   26.22 -      (if super then Graph.imm_succs else Graph.imm_preds) coes_graph T
   26.23 +      (if super then Graph.immediate_succs else Graph.immediate_preds) coes_graph T
   26.24          handle Graph.UNDEF _ => [];
   26.25  
   26.26      fun minmax sup (T :: Ts) =