Added function all_paths (formerly find_paths).

--- a/src/Pure/General/graph.ML	Fri Sep 22 13:04:30 2006 +0200
+++ b/src/Pure/General/graph.ML	Fri Sep 22 14:30:37 2006 +0200
@@ -40,6 +40,7 @@
   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
     'a T * 'a T -> 'a T                                               (*exception DUPS*)
   val irreducible_paths: 'a T -> key * key -> key list list
+  val all_paths: 'a T -> key * key -> key list list
   exception CYCLES of key list list
   val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
   val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
@@ -223,6 +224,19 @@
   in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end;
 
 
+(* find ALL paths from x to y *)
+
+fun all_paths G (x, y) =
+  let
+    val (_, X) = reachable (imm_succs G) [x];
+    fun paths ps p =
+      if not (null ps) andalso eq_key (p, x) then [p :: ps]
+      else if member_keys X p andalso not (member_key ps p)
+      then List.concat (map (paths (p :: ps)) (imm_preds G p))
+      else [];
+  in paths [] y end;
+
+
 (* maintain acyclic graphs *)
 
 exception CYCLES of key list list;