src/Pure/Tools/class_deps.ML
changeset 58201 5bf56c758e02
child 58202 be1d10595b7b
equal deleted inserted replaced
58200:d95055489fce 58201:5bf56c758e02
       
     1 (*  Title:      Pure/Tools/class_deps.ML
       
     2     Author:     Florian Haftmann, TU Muenchen
       
     3 
       
     4 Visualization of class dependencies.
       
     5 *)
       
     6 
       
     7 signature CLASS_DEPS =
       
     8 sig
       
     9   val class_deps: Toplevel.transition -> Toplevel.transition
       
    10 end;
       
    11 
       
    12 structure Class_deps: CLASS_DEPS =
       
    13 struct
       
    14 
       
    15 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
       
    16   let
       
    17     val ctxt = Toplevel.context_of state;
       
    18     val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
       
    19     val classes = Sorts.classes_of algebra;
       
    20     fun entry (c, (i, (_, cs))) =
       
    21       (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
       
    22             dir = "", unfold = true, path = "", content = []});
       
    23     val gr =
       
    24       Graph.fold (cons o entry) classes []
       
    25       |> sort (int_ord o pairself #1) |> map #2;
       
    26   in Graph_Display.display_graph gr end);
       
    27 
       
    28 val _ =
       
    29   Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
       
    30     (Scan.succeed class_deps);
       
    31 
       
    32 end;