933 |> subtract (op =) xs |
933 |> subtract (op =) xs |
934 |> map y_for |
934 |> map y_for |
935 |> distinct (op =); |
935 |> distinct (op =); |
936 val succs = map (fn (xs, _) => (xs, coalesced_succs_for xs)) xss_ys; |
936 val succs = map (fn (xs, _) => (xs, coalesced_succs_for xs)) xss_ys; |
937 in |
937 in |
938 map (fn (xs, y) => ((y, xs), (the o AList.lookup (op =) succs) xs)) xss_ys |
938 map (fn (xs, y) => ((y, xs), (maps (Graph.get_node gr) xs, (the o AList.lookup (op =) succs) xs))) xss_ys |
939 end; |
939 end; |
940 |
940 |
941 fun code_deps ctxt consts = |
941 fun code_deps ctxt consts = |
942 let |
942 let |
943 val thy = Proof_Context.theory_of ctxt; |
943 val thy = Proof_Context.theory_of ctxt; |
944 val namify = commas o map (Code.string_of_const thy); |
944 fun mk_entry ((name, consts), (ps, deps)) = |
|
945 let |
|
946 val label = commas (map (Code.string_of_const thy) consts); |
|
947 in ((name, Graph_Display.content_node label (Pretty.str label :: ps)), deps) end; |
945 in |
948 in |
946 code_depgr ctxt consts |
949 code_depgr ctxt consts |
947 |> Graph.map (fn c => fn _ => c) |
950 |> Graph.map (K (Code.pretty_cert thy o snd)) |
948 |> coalesce_strong_conn |
951 |> coalesce_strong_conn |
949 |> map (fn ((name, consts), deps) => ((name, Graph_Display.content_node (namify consts) []), deps)) |
952 |> map mk_entry |
950 |> Graph_Display.display_graph |
953 |> Graph_Display.display_graph |
951 end; |
954 end; |
952 |
955 |
953 local |
956 local |
954 |
957 |