added class_deps;
authorwenzelm
Mon Sep 18 19:12:46 2006 +0200 (2006-09-18 ago)
changeset 20574a10885a269cb
parent 20573 c945a208e7f8
child 20575 6b1c69265331
added class_deps;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Sep 18 19:12:45 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Sep 18 19:12:46 2006 +0200
     1.3 @@ -57,8 +57,8 @@
     1.4    val print_trans_rules: Toplevel.transition -> Toplevel.transition
     1.5    val print_methods: Toplevel.transition -> Toplevel.transition
     1.6    val print_antiquotations: Toplevel.transition -> Toplevel.transition
     1.7 -  val thm_deps: (thmref * Attrib.src list) list ->
     1.8 -    Toplevel.transition -> Toplevel.transition
     1.9 +  val class_deps: Toplevel.transition -> Toplevel.transition
    1.10 +  val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
    1.11    val find_theorems: int option * (bool * string FindTheorems.criterion) list
    1.12      -> Toplevel.transition -> Toplevel.transition
    1.13    val print_binds: Toplevel.transition -> Toplevel.transition
    1.14 @@ -269,6 +269,19 @@
    1.15  
    1.16  val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations;
    1.17  
    1.18 +val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.19 +  let
    1.20 +    val thy = Toplevel.theory_of state;
    1.21 +    val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
    1.22 +    val {classes, ...} = Sorts.rep_algebra algebra;
    1.23 +    fun entry (c, (i, (_, cs))) =
    1.24 +      (i, {name = NameSpace.extern space c, ID = c, parents = cs,
    1.25 +            dir = "", unfold = true, path = ""});
    1.26 +    val gr =
    1.27 +      Graph.fold (cons o entry) classes []
    1.28 +      |> sort (int_ord o pairself #1) |> map #2;
    1.29 +  in Present.display_graph gr end);
    1.30 +
    1.31  
    1.32  (* retrieve theorems *)
    1.33  
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Sep 18 19:12:45 2006 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Sep 18 19:12:46 2006 +0200
     2.3 @@ -717,6 +717,10 @@
     2.4    OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag
     2.5      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
     2.6  
     2.7 +val class_depsP =
     2.8 +  OuterSyntax.improper_command "class_deps" "visualize class dependencies"
     2.9 +    K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
    2.10 +
    2.11  val thm_depsP =
    2.12    OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
    2.13      K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
    2.14 @@ -914,10 +918,10 @@
    2.15    print_syntaxP, print_theoremsP, print_localesP, print_localeP,
    2.16    print_registrationsP, print_attributesP, print_simpsetP,
    2.17    print_rulesP, print_induct_rulesP, print_trans_rulesP,
    2.18 -  print_methodsP, print_antiquotationsP, thm_depsP, find_theoremsP,
    2.19 -  print_bindsP, print_lthmsP, print_casesP, print_stmtsP, print_thmsP,
    2.20 -  print_prfsP, print_full_prfsP, print_propP, print_termP,
    2.21 -  print_typeP,
    2.22 +  print_methodsP, print_antiquotationsP, class_depsP, thm_depsP,
    2.23 +  find_theoremsP, print_bindsP, print_lthmsP, print_casesP,
    2.24 +  print_stmtsP, print_thmsP, print_prfsP, print_full_prfsP,
    2.25 +  print_propP, print_termP, print_typeP,
    2.26    (*system commands*)
    2.27    cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
    2.28    touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,