# HG changeset patch # User wenzelm # Date 1429184890 -7200 # Node ID c48d536231fee1d23875619090d25bea9cae1a7f # Parent 20d437414174c4a4812a66e8ec9fd299eefdfd5d clarified thy_deps; diff -r 20d437414174 -r c48d536231fe NEWS --- a/NEWS Thu Apr 16 13:39:21 2015 +0200 +++ b/NEWS Thu Apr 16 13:48:10 2015 +0200 @@ -77,6 +77,9 @@ * Improved graphview panel with optional output of PNG or PDF, for display of 'thy_deps', 'locale_deps', 'class_deps' etc. +* Command 'thy_deps' allows optional bounds, analogously to +'class_deps'. + * Improved scheduling for asynchronous print commands (e.g. provers managed by the Sledgehammer panel) wrt. ongoing document processing. diff -r 20d437414174 -r c48d536231fe src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Thu Apr 16 13:39:21 2015 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Thu Apr 16 13:48:10 2015 +0200 @@ -25,6 +25,7 @@ \begin{matharray}{rcl} @{command_def "theory"} & : & @{text "toplevel \ theory"} \\ @{command_def (global) "end"} & : & @{text "theory \ toplevel"} \\ + @{command_def "thy_deps"}@{text "\<^sup>*"} & : & @{text "theory \"} \\ \end{matharray} Isabelle/Isar theories are defined via theory files, which consist of an @@ -64,6 +65,10 @@ ; keyword_decls: (@{syntax string} +) ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})? + ; + @@{command thy_deps} (thy_bounds thy_bounds?)? + ; + thy_bounds: @{syntax name} | '(' (@{syntax name} + @'|') ')' \} \begin{description} @@ -104,6 +109,12 @@ @{keyword "begin"} that needs to be matched by @{command (local) "end"}, according to the usual rules for nested blocks. + \item @{command thy_deps} visualizes the theory hierarchy as a directed + acyclic graph. By default, all imported theories are shown, taking the + base session as a starting point. Alternatively, it is possibly to + restrict the full theory graph by giving bounds, analogously to + @{command_ref class_deps}. + \end{description} \ diff -r 20d437414174 -r c48d536231fe src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Apr 16 13:39:21 2015 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Thu Apr 16 13:48:10 2015 +0200 @@ -35,7 +35,6 @@ val diag_state: Proof.context -> Toplevel.state val diag_goal: Proof.context -> {context: Proof.context, facts: thm list, goal: thm} val pretty_theorems: bool -> Toplevel.state -> Pretty.T list - val thy_deps: Toplevel.transition -> Toplevel.transition val locale_deps: Toplevel.transition -> Toplevel.transition val print_stmts: string list * (Facts.ref * Token.src list) list -> Toplevel.transition -> Toplevel.transition @@ -270,15 +269,6 @@ (* display dependencies *) -val thy_deps = - Toplevel.unknown_theory o - Toplevel.keep (fn st => - let - val thy = Toplevel.theory_of st; - val parent_session = Session.get_name (); - val parent_loaded = is_some o Thy_Info.lookup_theory; - in Graph_Display.display_graph (Present.session_graph parent_session parent_loaded thy) end); - val locale_deps = Toplevel.unknown_theory o Toplevel.keep (Toplevel.theory_of #> (fn thy => diff -r 20d437414174 -r c48d536231fe src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Thu Apr 16 13:39:21 2015 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Apr 16 13:48:10 2015 +0200 @@ -800,10 +800,6 @@ Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of))); val _ = - Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies" - (Scan.succeed Isar_Cmd.thy_deps); - -val _ = Outer_Syntax.command @{command_keyword locale_deps} "visualize locale dependencies" (Scan.succeed Isar_Cmd.locale_deps); diff -r 20d437414174 -r c48d536231fe src/Pure/Pure.thy --- a/src/Pure/Pure.thy Thu Apr 16 13:39:21 2015 +0200 +++ b/src/Pure/Pure.thy Thu Apr 16 13:48:10 2015 +0200 @@ -98,6 +98,7 @@ ML_file "Tools/rail.ML" ML_file "Tools/rule_insts.ML" ML_file "Tools/thm_deps.ML" +ML_file "Tools/thy_deps.ML" ML_file "Tools/class_deps.ML" ML_file "Tools/find_theorems.ML" ML_file "Tools/find_consts.ML" diff -r 20d437414174 -r c48d536231fe src/Pure/Tools/thy_deps.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/thy_deps.ML Thu Apr 16 13:48:10 2015 +0200 @@ -0,0 +1,50 @@ +(* Title: Pure/Tools/thy_deps.ML + Author: Makarius + +Visualization of theory dependencies. +*) + +signature THY_DEPS = +sig + val thy_deps: theory -> theory list option * theory list option -> Graph_Display.entry list + val thy_deps_cmd: theory -> string list option * string list option -> unit +end; + +structure Thy_Deps: THY_DEPS = +struct + +fun gen_thy_deps _ thy0 (NONE, NONE) = + let + val parent_session = Session.get_name (); + val parent_loaded = is_some o Thy_Info.lookup_theory; + in Present.session_graph parent_session parent_loaded thy0 end + | gen_thy_deps prep_thy thy0 bounds = + let + val (upper, lower) = apply2 ((Option.map o map) (prep_thy thy0)) bounds; + val rel = Theory.subthy o swap; + val pred = + (case upper of + SOME Bs => (fn thy => exists (fn B => rel (thy, B)) Bs) + | NONE => K true) andf + (case lower of + SOME Bs => (fn thy => exists (fn B => rel (B, thy)) Bs) + | NONE => K true); + fun node thy = + ((Context.theory_name thy, Graph_Display.content_node (Context.theory_name thy) []), + map Context.theory_name (filter pred (Theory.parents_of thy))); + in Theory.nodes_of thy0 |> filter pred |> map node end; + +val thy_deps = gen_thy_deps (K I); +val thy_deps_cmd = Graph_Display.display_graph oo gen_thy_deps Context.get_theory; + +val theory_bounds = + Parse.theory_xname >> single || + (@{keyword "("} |-- Parse.enum "|" Parse.theory_xname --| @{keyword ")"}); + +val _ = + Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies" + (Scan.option theory_bounds -- Scan.option theory_bounds >> (fn args => + (Toplevel.unknown_theory o + Toplevel.keep (fn st => thy_deps_cmd (Toplevel.theory_of st) args)))); + +end;