# HG changeset patch
# User wenzelm
# Date 1167409486 -3600
# Node ID 4e20a5397b57bf3cfec1d967c515165184b4476c
# Parent  ba683b0b245624cc33247d46399448f78150faeb
renamed project to subgraph, improved presentation, avoided unnecessary evaluation of predicate;

diff -r ba683b0b2456 -r 4e20a5397b57 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Fri Dec 29 17:24:45 2006 +0100
+++ b/src/Pure/General/graph.ML	Fri Dec 29 17:24:46 2006 +0100
@@ -19,6 +19,7 @@
   val fold: (key * ('a * (key list * key list)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
   val minimals: 'a T -> key list
   val maximals: 'a T -> key list
+  val subgraph: (key -> bool) -> 'a T -> 'a T
   val map_nodes: ('a -> 'b) -> 'a T -> 'b T
   val fold_map_nodes: (key * 'a -> 'b -> 'c * 'b) -> 'a T -> 'b -> 'c T * 'b
   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
@@ -29,7 +30,6 @@
   val all_preds: 'a T -> key list -> key list
   val all_succs: 'a T -> key list -> key list
   val strong_conn: 'a T -> key list list
-  val project: (key -> bool) -> 'a T -> 'a T
   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
   val default_node: key * 'a -> 'a T -> 'a T
   val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
@@ -91,6 +91,12 @@
 fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G [];
 fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m | _ => I) G [];
 
+fun subgraph P G =
+  let
+    fun subg (k, (i, (preds, succs))) =
+      if P k then Table.update (k, (i, (filter P preds, filter P succs))) else I;
+  in Graph (fold_graph subg G Table.empty) end;
+
 fun get_entry (Graph tab) x =
   (case Table.lookup tab x of
     SOME entry => entry
@@ -141,13 +147,6 @@
 fun strong_conn G = filter_out null (fst (reachable (imm_preds G)
   (flat (rev (fst (reachable (imm_succs G) (keys G)))))));
 
-(*subgraph induced by node subset*)
-fun project proj G =
-  let
-    fun subg (k, (i, (preds, succs))) =
-      proj k ? Table.update (k, (i, (filter proj preds, filter proj succs)));
-  in Graph (fold_graph subg G Table.empty) end;
-
 
 (* nodes *)