--- 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>\<open>thm_deps\<close> "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>\<open>thm_oracles\<close>
@@ -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])
--- 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