clarified thy_deps;

--- 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.
 

--- 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 \<rightarrow> theory"} \\
     @{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
+    @{command_def "thy_deps"}@{text "\<^sup>*"} & : & @{text "theory \<rightarrow>"} \\
   \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} + @'|') ')'
   \<close>}
 
   \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}
 \<close>
 

--- 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 =>

--- 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);
 

--- 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"

--- /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;