# 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>\locale\ or \<^theory_text>\class\ may involve a \<^theory_text>\begin\ that needs to be matched by @{command (local) "end"}, according to the usual rules for nested blocks. \<^descr> \<^theory_text>\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}. + By default, all imported theories are shown. This may be restricted by + specifying bounds wrt. the theory inclusion relation. \ @@ -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>\private\ or \<^theory_text>\qualified\ 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>\context begin \ end\ 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 \c\ with parameter \x\ and assumption \A[x]\. - + 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, \a \ t[x]\ becomes \c.a ?x \ @@ -321,7 +320,7 @@ object-logic. This usually covers object-level equality \x = y\ and equivalence \A \ B\. 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.\ \f x y = t\ instead of \f \ \x y. t\ and \y \ 0 \ g x y = u\ instead of an unrestricted \g \ \x y. u\. @@ -331,18 +330,18 @@ \<^descr> \<^theory_text>\abbreviation c where eq\ introduces a syntactic constant which is associated with a certain term according to the meta-level equality \eq\. - + 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 \mode\ specification restricts output to a particular print mode; using ``\input\'' here achieves the effect of one-way abbreviations. The mode may also include an ``\<^theory_text>\output\'' qualifier that affects the concrete syntax declared for abbreviations, cf.\ \<^theory_text>\syntax\ in \secref{sec:syn-trans}. - + \<^descr> \<^theory_text>\print_abbrevs\ prints all constant abbreviations of the current context; the ``\!\'' option indicates extra verbosity. \ @@ -574,12 +573,12 @@ the locale specification. When defining an operation derived from the parameters, \<^theory_text>\definition\ (\secref{sec:term-definitions}) is usually more appropriate. - + Note that ``\<^theory_text>\(is p\<^sub>1 \ p\<^sub>n)\'' 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 \loc_axioms\ 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 \loc\ 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>\ML_val\ and \<^theory_text>\ML_command\ are diagnostic versions of \<^theory_text>\ML\, which means that the context may not be updated. \<^theory_text>\ML_val\ echos the bindings produced at the ML toplevel, but \<^theory_text>\ML_command\ is silent. - + \<^descr> \<^theory_text>\setup "text"\ changes the current theory context by applying \text\, 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 @@ \\<^sub>n) t\ for the existing type \\\. 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>\typedecl (\\<^sub>1, \, \\<^sub>n) t\ declares a new type constructor \t\. If the object-logic defines a base sort \s\, then the constructor is declared to operate on that, via the axiomatic type-class instance \t :: (s, \, s)s\. 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 =>