equal
deleted
inserted
replaced
28 fun entry (c, (i, (_, cs))) = |
28 fun entry (c, (i, (_, cs))) = |
29 (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs, |
29 (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs, |
30 dir = "", unfold = true, path = "", content = []}); |
30 dir = "", unfold = true, path = "", content = []}); |
31 val gr = |
31 val gr = |
32 Graph.fold (cons o entry) classes [] |
32 Graph.fold (cons o entry) classes [] |
33 |> sort (int_ord o pairself #1) |> map #2; |
33 |> sort (int_ord o apply2 #1) |> map #2; |
34 in Graph_Display.display_graph gr end; |
34 in Graph_Display.display_graph gr end; |
35 |
35 |
36 val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of); |
36 val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of); |
37 val visualize_cmd = gen_visualize Syntax.read_sort; |
37 val visualize_cmd = gen_visualize Syntax.read_sort; |
38 |
38 |