code equations as displayable content in code dependency graph
authorwenzelm
Mon Apr 27 16:46:52 2015 +0200 (2015-04-27)
changeset 60204137b3fc46bb3
parent 60203 add72fdadd0b
child 60205 9ee125c3bff7
code equations as displayable content in code dependency graph
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Apr 27 15:53:11 2015 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Apr 27 16:46:52 2015 +0200
     1.3 @@ -935,18 +935,21 @@
     1.4        |> distinct (op =);
     1.5      val succs = map (fn (xs, _) => (xs, coalesced_succs_for xs)) xss_ys;
     1.6    in
     1.7 -    map (fn (xs, y) => ((y, xs), (the o AList.lookup (op =) succs) xs)) xss_ys
     1.8 +    map (fn (xs, y) => ((y, xs), (maps (Graph.get_node gr) xs, (the o AList.lookup (op =) succs) xs))) xss_ys
     1.9    end;
    1.10  
    1.11  fun code_deps ctxt consts =
    1.12    let
    1.13      val thy = Proof_Context.theory_of ctxt;
    1.14 -    val namify = commas o map (Code.string_of_const thy);
    1.15 +    fun mk_entry ((name, consts), (ps, deps)) =
    1.16 +      let
    1.17 +        val label = commas (map (Code.string_of_const thy) consts);
    1.18 +      in ((name, Graph_Display.content_node label (Pretty.str label :: ps)), deps) end;
    1.19    in
    1.20      code_depgr ctxt consts
    1.21 -    |> Graph.map (fn c => fn _ => c)
    1.22 +    |> Graph.map (K (Code.pretty_cert thy o snd))
    1.23      |> coalesce_strong_conn
    1.24 -    |> map (fn ((name, consts), deps) => ((name, Graph_Display.content_node (namify consts) []), deps))
    1.25 +    |> map mk_entry
    1.26      |> Graph_Display.display_graph
    1.27    end;
    1.28