# HG changeset patch
# User haftmann
# Date 1129735192 -7200
# Node ID 410ec3b7e771b4b222d238d86bf1410b719fd577
# Parent  fbe857bedcd7cc73118ce16f2aab35caeec714be
added subgraph

diff -r fbe857bedcd7 -r 410ec3b7e771 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Wed Oct 19 17:19:37 2005 +0200
+++ b/src/Pure/General/graph.ML	Wed Oct 19 17:19:52 2005 +0200
@@ -28,6 +28,7 @@
   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 subgraph: key list -> 'a T -> 'a T
   val find_paths: 'a T -> key * key -> key list list
   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
   val default_node: key * 'a -> 'a T -> 'a T
@@ -140,6 +141,15 @@
 fun strong_conn G = filter_out null (snd (reachable (imm_preds G)
   (List.concat (rev (snd (reachable (imm_succs G) (keys G)))))));
 
+(*subgraph induced by node subset*)
+fun subgraph keys (Graph tab) =
+  let
+    val select = member eq_key keys;
+    fun subg (k, (i, (preds, succs))) tab' =
+      if select k
+      then tab' |> Table.update (k, (i, (filter select preds, filter select succs)))
+      else tab'
+  in Table.empty |> Table.fold subg tab |> Graph end;
 
 (* paths *)