# HG changeset patch
# User wenzelm
# Date 1492434501 -7200
# Node ID 7fb81fa1d668d593fa618c7f9ac8dea5ce8e1a13
# Parent  571a3ce3cc17fbd1e8a357c1cd024fc6a55fa0e9
more uniform thy_deps (like class_deps), see also c48d536231fe;

diff -r 571a3ce3cc17 -r 7fb81fa1d668 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Apr 17 13:14:01 2017 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Apr 17 15:08:21 2017 +0200
@@ -101,16 +101,15 @@
   for syntactic completion. The default for a new keyword is just its name,
   but completion may be avoided by defining @{keyword "abbrevs"} with empty
   text.
-  
+
   \<^descr> @{command (global) "end"} concludes the current theory definition. Note
   that some other commands, e.g.\ local theory targets \<^theory_text>\<open>locale\<close> or \<^theory_text>\<open>class\<close>
   may involve a \<^theory_text>\<open>begin\<close> that needs to be matched by @{command (local) "end"},
   according to the usual rules for nested blocks.
 
   \<^descr> \<^theory_text>\<open>thy_deps\<close> 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}.
+  By default, all imported theories are shown. This may be restricted by
+  specifying bounds wrt. the theory inclusion relation.
 \<close>
 
 
@@ -157,11 +156,11 @@
   means any results stemming from definitions and proofs in the extended
   context will be exported into the enclosing target by lifting over extra
   parameters and premises.
-  
+
   \<^descr> @{command (local) "end"} concludes the current local theory, according to
   the nesting of contexts. Note that a global @{command (global) "end"} has a
   different meaning: it concludes the theory itself (\secref{sec:begin-thy}).
-  
+
   \<^descr> \<^theory_text>\<open>private\<close> or \<^theory_text>\<open>qualified\<close> may be given as modifiers before any local
   theory command. This restricts name space accesses to the local scope, as
   determined by the enclosing \<^theory_text>\<open>context begin \<dots> end\<close> block. Outside its scope,
@@ -189,7 +188,7 @@
   on the underlying target infrastructure (locale, type class etc.). The
   general idea is as follows, considering a context named \<open>c\<close> with parameter
   \<open>x\<close> and assumption \<open>A[x]\<close>.
-  
+
   Definitions are exported by introducing a global version with additional
   arguments; a syntactic abbreviation links the long form with the abstract
   version of the target context. For example, \<open>a \<equiv> t[x]\<close> becomes \<open>c.a ?x \<equiv>
@@ -321,7 +320,7 @@
   object-logic. This usually covers object-level equality \<open>x = y\<close> and
   equivalence \<open>A \<longleftrightarrow> B\<close>. End-users normally need not change the @{attribute
   defn} setup.
-  
+
   Definitions may be presented with explicit arguments on the LHS, as well as
   additional conditions, e.g.\ \<open>f x y = t\<close> instead of \<open>f \<equiv> \<lambda>x y. t\<close> and \<open>y \<noteq> 0
   \<Longrightarrow> g x y = u\<close> instead of an unrestricted \<open>g \<equiv> \<lambda>x y. u\<close>.
@@ -331,18 +330,18 @@
 
   \<^descr> \<^theory_text>\<open>abbreviation c where eq\<close> introduces a syntactic constant which is
   associated with a certain term according to the meta-level equality \<open>eq\<close>.
-  
+
   Abbreviations participate in the usual type-inference process, but are
   expanded before the logic ever sees them. Pretty printing of terms involves
   higher-order rewriting with rules stemming from reverted abbreviations. This
   needs some care to avoid overlapping or looping syntactic replacements!
-  
+
   The optional \<open>mode\<close> specification restricts output to a particular print
   mode; using ``\<open>input\<close>'' here achieves the effect of one-way abbreviations.
   The mode may also include an ``\<^theory_text>\<open>output\<close>'' qualifier that affects the
   concrete syntax declared for abbreviations, cf.\ \<^theory_text>\<open>syntax\<close> in
   \secref{sec:syn-trans}.
-  
+
   \<^descr> \<^theory_text>\<open>print_abbrevs\<close> prints all constant abbreviations of the current context;
   the ``\<open>!\<close>'' option indicates extra verbosity.
 \<close>
@@ -574,12 +573,12 @@
   the locale specification. When defining an operation derived from the
   parameters, \<^theory_text>\<open>definition\<close> (\secref{sec:term-definitions}) is usually more
   appropriate.
-  
+
   Note that ``\<^theory_text>\<open>(is p\<^sub>1 \<dots> p\<^sub>n)\<close>'' patterns given in the syntax of @{element
   "assumes"} and @{element "defines"} above are illegal in locale definitions.
   In the long goal format of \secref{sec:goals}, term bindings may be included
   as expected, though.
-  
+
   \<^medskip>
   Locale specifications are ``closed up'' by turning the given text into a
   predicate definition \<open>loc_axioms\<close> and deriving the original assumptions as
@@ -587,7 +586,7 @@
   the newly specified assumptions, omitting the content of included locale
   expressions. The full cumulative view is only provided on export, involving
   another predicate \<open>loc\<close> that refers to the complete specification text.
-  
+
   In any case, the predicate arguments are those locale parameters that
   actually occur in the respective piece of text. Also these predicates
   operate at the meta-level in theory, but the locale packages attempts to
@@ -1111,7 +1110,7 @@
   \<^descr> \<^theory_text>\<open>ML_val\<close> and \<^theory_text>\<open>ML_command\<close> are diagnostic versions of \<^theory_text>\<open>ML\<close>, which means
   that the context may not be updated. \<^theory_text>\<open>ML_val\<close> echos the bindings produced
   at the ML toplevel, but \<^theory_text>\<open>ML_command\<close> is silent.
-  
+
   \<^descr> \<^theory_text>\<open>setup "text"\<close> changes the current theory context by applying \<open>text\<close>,
   which refers to an ML expression of type @{ML_type "theory -> theory"}. This
   enables to initialize any object-logic specific tools and packages written
@@ -1223,7 +1222,7 @@
   \<alpha>\<^sub>n) t\<close> for the existing type \<open>\<tau>\<close>. Unlike the semantic type definitions in
   Isabelle/HOL, type synonyms are merely syntactic abbreviations without any
   logical significance. Internally, type synonyms are fully expanded.
-  
+
   \<^descr> \<^theory_text>\<open>typedecl (\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t\<close> declares a new type constructor \<open>t\<close>. If the
   object-logic defines a base sort \<open>s\<close>, then the constructor is declared to
   operate on that, via the axiomatic type-class instance \<open>t :: (s, \<dots>, s)s\<close>.
diff -r 571a3ce3cc17 -r 7fb81fa1d668 src/Pure/Tools/thy_deps.ML
--- a/src/Pure/Tools/thy_deps.ML	Mon Apr 17 13:14:01 2017 +0200
+++ b/src/Pure/Tools/thy_deps.ML	Mon Apr 17 15:08:21 2017 +0200
@@ -6,7 +6,8 @@
 
 signature THY_DEPS =
 sig
-  val thy_deps: Proof.context -> theory list option * theory list option -> Graph_Display.entry list
+  val thy_deps: Proof.context -> theory list option * theory list option ->
+    Graph_Display.entry list
   val thy_deps_cmd: Proof.context ->
     (string * Position.T) list option * (string * Position.T) list option -> unit
 end;
@@ -14,26 +15,21 @@
 structure Thy_Deps: THY_DEPS =
 struct
 
-fun gen_thy_deps _ ctxt (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 (Proof_Context.theory_of ctxt) end
-  | gen_thy_deps prep_thy ctxt bounds =
-      let
-        val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
-        val rel = Context.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 map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
+fun gen_thy_deps prep_thy ctxt bounds =
+  let
+    val (upper, lower) = apply2 ((Option.map o map) (prep_thy ctxt)) bounds;
+    val rel = Context.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 map node (filter pred (Theory.nodes_of (Proof_Context.theory_of ctxt))) end;
 
 val thy_deps =
   gen_thy_deps (fn ctxt => fn thy =>