--- a/src/Pure/Isar/isar_cmd.ML Thu Jul 27 18:25:44 2000 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Thu Jul 27 18:25:55 2000 +0200
@@ -51,6 +51,7 @@
val print_methods: Toplevel.transition -> Toplevel.transition
val print_antiquotations: Toplevel.transition -> Toplevel.transition
val print_thms_containing: xstring list -> Toplevel.transition -> Toplevel.transition
+ val thm_deps: (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition
val print_binds: Toplevel.transition -> Toplevel.transition
val print_lthms: Toplevel.transition -> Toplevel.transition
val print_cases: Toplevel.transition -> Toplevel.transition
@@ -178,6 +179,9 @@
fun print_thms_containing cs = Toplevel.keep (fn state =>
ThmDatabase.print_thms_containing (Toplevel.theory_of state) cs);
+fun thm_deps args = Toplevel.keep (fn state =>
+ ThmDeps.thm_deps (IsarThy.get_thmss args (Toplevel.enter_forward_proof state)));
+
(* print proof context contents *)
@@ -215,7 +219,7 @@
in with_modes ms (fn () => Pretty.string_of (Pretty.quote (Sign.pretty_typ sign T))) end;
fun print_item string_of (x, y) = Toplevel.keep (fn state =>
- writeln (string_of (Toplevel.node_case Proof.init_state Proof.enter_forward state) x y));
+ writeln (string_of (Toplevel.enter_forward_proof state) x y));
val print_thms = print_item string_of_thms;
val print_prop = print_item string_of_prop;
--- a/src/Pure/Isar/isar_syn.ML Thu Jul 27 18:25:44 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Jul 27 18:25:55 2000 +0200
@@ -538,6 +538,10 @@
OuterSyntax.improper_command "thms_containing" "print theorems containing all given constants"
K.diag (Scan.repeat P.xname >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
+val thm_depsP =
+ OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
+ K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
+
val print_bindsP =
OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
(Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
@@ -683,8 +687,8 @@
pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
print_syntaxP, print_theoremsP, print_attributesP,
print_trans_rulesP, print_methodsP, print_antiquotationsP,
- thms_containingP, print_bindsP, print_lthmsP, print_casesP,
- print_thmsP, print_propP, print_termP, print_typeP,
+ thms_containingP, thm_depsP, print_bindsP, print_lthmsP,
+ print_casesP, print_thmsP, print_propP, print_termP, print_typeP,
(*system commands*)
cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,