further graph operations from ML;

--- a/src/Pure/General/graph.ML	Thu Feb 23 14:46:38 2012 +0100
+++ b/src/Pure/General/graph.ML	Thu Feb 23 15:15:59 2012 +0100
@@ -37,11 +37,11 @@
   val immediate_succs: 'a T -> key -> key list
   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 minimals: 'a T -> key list
   val maximals: 'a T -> key list
   val is_minimal: 'a T -> key -> bool
   val is_maximal: 'a T -> key -> bool
-  val strong_conn: 'a T -> key list list
   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*)
@@ -169,17 +169,19 @@
 fun all_preds G = flat o #1 o reachable (imm_preds G);
 fun all_succs G = flat o #1 o reachable (imm_succs G);
 
-(*minimal and maximal elements*)
+(*strongly connected components; see: David King and John Launchbury,
+  "Structuring Depth First Search Algorithms in Haskell"*)
+fun strong_conn G =
+  rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
+
+
+(* minimal and maximal elements *)
+
 fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G [];
 fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G [];
 fun is_minimal G x = Keys.is_empty (imm_preds G x);
 fun is_maximal G x = Keys.is_empty (imm_succs G x);
 
-(*strongly connected components; see: David King and John Launchbury,
-  "Structuring Depth First Search Algorithms in Haskell"*)
-fun strong_conn G =
-  rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
-
 
 (* nodes *)
 

--- a/src/Pure/General/graph.scala	Thu Feb 23 14:46:38 2012 +0100
+++ b/src/Pure/General/graph.scala	Thu Feb 23 15:15:59 2012 +0100
@@ -91,6 +91,11 @@
   def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten
   def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten
 
+  /*strongly connected components; see: David King and John Launchbury,
+    "Structuring Depth First Search Algorithms in Haskell"*/
+  def strong_conn: List[List[Key]] =
+    reachable(imm_preds, all_succs(keys.toList))._1.filterNot(_.isEmpty).reverse
+
 
   /* minimal and maximal elements */
 
@@ -114,6 +119,12 @@
     else new Graph[Key, A](rep + (x -> (info, (Set.empty, Set.empty))))
   }
 
+  def default_node(x: Key, info: A): Graph[Key, A] =
+  {
+    if (rep.isDefinedAt(x)) this
+    else new_node(x, info)
+  }
+
   def del_nodes(xs: List[Key]): Graph[Key, A] =
   {
     xs.foreach(get_entry)