# HG changeset patch
# Parent 93cc5c17433878ef212a68d309564da9c8df8fc9
code equations as displayable content in code dependency graph

diff -r 93cc5c174338 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sun Apr 26 11:35:07 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML	Sun Apr 26 17:12:42 2015 +0200
@@ -935,18 +935,21 @@
       |> distinct (op =);
     val succs = map (fn (xs, _) => (xs, coalesced_succs_for xs)) xss_ys;
   in
-    map (fn (xs, y) => ((y, xs), (the o AList.lookup (op =) succs) xs)) xss_ys
+    map (fn (xs, y) => ((y, xs), (maps (Graph.get_node gr) xs, (the o AList.lookup (op =) succs) xs))) xss_ys
   end;
 
 fun code_deps ctxt consts =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val namify = commas o map (Code.string_of_const thy);
+    fun mk_entry ((name, consts), (ps, deps)) =
+      let
+        val label = commas (map (Code.string_of_const thy) consts);
+      in ((name, Graph_Display.content_node label (Pretty.str label :: ps)), deps) end;
   in
     code_depgr ctxt consts
-    |> Graph.map (fn c => fn _ => c)
+    |> Graph.map (K (Code.pretty_cert thy o snd))
     |> coalesce_strong_conn
-    |> map (fn ((name, consts), deps) => ((name, Graph_Display.content_node (namify consts) []), deps))
+    |> map mk_entry
     |> Graph_Display.display_graph
   end;