# HG changeset patch
# User haftmann
# Date 1238260641 -3600
# Node ID 756088c52d109f75a32163a9d13182bd46b1b9ee
# Parent  16c689643a7a3f0e001acbc47b2b9bb6c46cbf14
second attempt for code_deps command

diff -r 16c689643a7a -r 756088c52d10 src/Tools/code/code_wellsorted.ML
--- a/src/Tools/code/code_wellsorted.ML	Sat Mar 28 16:29:39 2009 +0100
+++ b/src/Tools/code/code_wellsorted.ML	Sat Mar 28 18:17:21 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