# HG changeset patch # User wenzelm # Date 1566061443 -7200 # Node ID d94456876f2d3d5900588d241f1be39642eebb5b # Parent 095dadc62bb536f3cbe7f34cfb85361531cdce28 clarified signature; diff -r 095dadc62bb5 -r d94456876f2d src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Aug 17 17:59:55 2019 +0200 +++ b/src/Pure/Pure.thy Sat Aug 17 19:04:03 2019 +0200 @@ -1304,8 +1304,10 @@ Outer_Syntax.command \<^command_keyword>\thm_deps\ "visualize theorem dependencies" (Parse.thms1 >> (fn args => Toplevel.keep (fn st => - Thm_Deps.thm_deps (Toplevel.theory_of st) - (Attrib.eval_thms (Toplevel.context_of st) args)))); + let + val thy = Toplevel.theory_of st; + val ctxt = Toplevel.context_of st; + in Thm_Deps.thm_deps_cmd thy (Attrib.eval_thms ctxt args) end))); val _ = Outer_Syntax.command \<^command_keyword>\thm_oracles\ @@ -1329,7 +1331,7 @@ fun pretty_thm (a, th) = Proof_Context.pretty_fact ctxt (a, [th]); val check = Theory.check {long = false} ctxt; in - Thm_Deps.unused_thms + Thm_Deps.unused_thms_cmd (case opt_range of NONE => (Theory.parents_of thy, [thy]) | SOME (xs, NONE) => (map check xs, [thy]) diff -r 095dadc62bb5 -r d94456876f2d src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Sat Aug 17 17:59:55 2019 +0200 +++ b/src/Pure/Thy/thm_deps.ML Sat Aug 17 19:04:03 2019 +0200 @@ -10,8 +10,8 @@ val all_oracles: thm list -> Proofterm.oracle list val has_skip_proof: thm list -> bool val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T - val thm_deps: theory -> thm list -> unit - val unused_thms: theory list * theory list -> (string * thm) list + val thm_deps_cmd: theory -> thm list -> unit + val unused_thms_cmd: theory list * theory list -> (string * thm) list end; structure Thm_Deps: THM_DEPS = @@ -35,9 +35,9 @@ in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end; -(* thm_deps *) +(* thm_deps_cmd *) -fun thm_deps thy thms = +fun thm_deps_cmd thy thms = let fun make_node name directory = Graph_Display.session_node @@ -70,9 +70,9 @@ end; -(* unused_thms *) +(* unused_thms_cmd *) -fun unused_thms (base_thys, thys) = +fun unused_thms_cmd (base_thys, thys) = let fun add_fact transfer space (name, ths) = if exists (fn thy => Global_Theory.defined_fact thy name) base_thys then I