# HG changeset patch # User wenzelm # Date 1158599566 -7200 # Node ID a10885a269cb762d29aa71eb2fbbc832c0e37e16 # Parent c945a208e7f8a9e8021504f8f0866ebd88e8840a added class_deps; diff -r c945a208e7f8 -r a10885a269cb src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Mon Sep 18 19:12:45 2006 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Mon Sep 18 19:12:46 2006 +0200 @@ -57,8 +57,8 @@ val print_trans_rules: Toplevel.transition -> Toplevel.transition val print_methods: Toplevel.transition -> Toplevel.transition val print_antiquotations: Toplevel.transition -> Toplevel.transition - val thm_deps: (thmref * Attrib.src list) list -> - Toplevel.transition -> Toplevel.transition + val class_deps: Toplevel.transition -> Toplevel.transition + val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition val find_theorems: int option * (bool * string FindTheorems.criterion) list -> Toplevel.transition -> Toplevel.transition val print_binds: Toplevel.transition -> Toplevel.transition @@ -269,6 +269,19 @@ val print_antiquotations = Toplevel.imperative IsarOutput.print_antiquotations; +val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state => + let + val thy = Toplevel.theory_of state; + val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy); + val {classes, ...} = Sorts.rep_algebra algebra; + fun entry (c, (i, (_, cs))) = + (i, {name = NameSpace.extern space c, ID = c, parents = cs, + dir = "", unfold = true, path = ""}); + val gr = + Graph.fold (cons o entry) classes [] + |> sort (int_ord o pairself #1) |> map #2; + in Present.display_graph gr end); + (* retrieve theorems *) diff -r c945a208e7f8 -r a10885a269cb src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Sep 18 19:12:45 2006 +0200 +++ b/src/Pure/Isar/isar_syn.ML Mon Sep 18 19:12:46 2006 +0200 @@ -717,6 +717,10 @@ OuterSyntax.improper_command "print_antiquotations" "print antiquotations (global)" K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations)); +val class_depsP = + OuterSyntax.improper_command "class_deps" "visualize class dependencies" + K.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps)); + val thm_depsP = OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies" K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps)); @@ -914,10 +918,10 @@ print_syntaxP, print_theoremsP, print_localesP, print_localeP, print_registrationsP, print_attributesP, print_simpsetP, print_rulesP, print_induct_rulesP, print_trans_rulesP, - print_methodsP, print_antiquotationsP, thm_depsP, find_theoremsP, - print_bindsP, print_lthmsP, print_casesP, print_stmtsP, print_thmsP, - print_prfsP, print_full_prfsP, print_propP, print_termP, - print_typeP, + print_methodsP, print_antiquotationsP, class_depsP, thm_depsP, + find_theoremsP, print_bindsP, print_lthmsP, print_casesP, + print_stmtsP, print_thmsP, print_prfsP, print_full_prfsP, + print_propP, print_termP, print_typeP, (*system commands*) cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP, touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,