# HG changeset patch
# User haftmann
# Date 1238260681 -3600
# Node ID a06b4404632837485c97eb79e69136194fc105d2
# Parent  b3c851b0ea39526fc6872a680b2a14fc2fc7b2e9# Parent  b27d167e5e54ac3c32311ca6a620c122a401a500
merged

diff -r b3c851b0ea39 -r a06b44046328 src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Sat Mar 28 16:33:32 2009 +0100
+++ b/src/Tools/code/code_wellsorted.ML	Sat Mar 28 18:18:01 2009 +0100
@@ -353,14 +353,20 @@
 fun code_deps thy consts =
   let
     val eqngr = code_depgr thy consts;
-    fun mk_entry (const, (_, (_, parents))) =
-      let
-        val name = Code_Unit.string_of_const thy const;
-        val nameparents = map (Code_Unit.string_of_const thy) parents;
-      in { name = name, ID = name, dir = "", unfold = true,
-        path = "", parents = nameparents }
-      end;
-    val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) eqngr [];
+    val constss = Graph.strong_conn eqngr;
+    val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
+      Symtab.update (const, consts)) consts) constss;
+    fun succs consts = consts
+      |> maps (Graph.imm_succs eqngr)
+      |> subtract (op =) consts
+      |> map (the o Symtab.lookup mapping)
+      |> distinct (op =);
+    val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
+    fun namify consts = map (Code_Unit.string_of_const thy) consts
+      |> commas;
+    val prgr = map (fn (consts, constss) =>
+      { name = namify consts, ID = namify consts, dir = "", unfold = true,
+        path = "", parents = map namify constss }) conn;
   in Present.display_graph prgr end;
 
 local