# HG changeset patch
# User berghofe
# Date 1204216415 -3600
# Node ID 64ee6a2ca6d68ae0d93a723b4bd62f40f25b9fbc
# Parent  0cc3ff184282a648c87801d5c344a8efaf80ac69
Added unused_thms command.

diff -r 0cc3ff184282 -r 64ee6a2ca6d6 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Thu Feb 28 16:54:56 2008 +0100
+++ b/etc/isar-keywords-ZF.el	Thu Feb 28 17:33:35 2008 +0100
@@ -193,6 +193,7 @@
     "undo"
     "undos_proof"
     "unfolding"
+    "unused_thms"
     "use"
     "use_thy"
     "using"
@@ -317,6 +318,7 @@
     "touch_child_thys"
     "touch_thy"
     "typ"
+    "unused_thms"
     "use"
     "use_thy"
     "value"
diff -r 0cc3ff184282 -r 64ee6a2ca6d6 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Feb 28 16:54:56 2008 +0100
+++ b/etc/isar-keywords.el	Thu Feb 28 17:33:35 2008 +0100
@@ -235,6 +235,7 @@
     "undo"
     "undos_proof"
     "unfolding"
+    "unused_thms"
     "use"
     "use_thy"
     "using"
@@ -385,6 +386,7 @@
     "touch_child_thys"
     "touch_thy"
     "typ"
+    "unused_thms"
     "use"
     "use_thy"
     "value"
diff -r 0cc3ff184282 -r 64ee6a2ca6d6 lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml	Thu Feb 28 16:54:56 2008 +0100
+++ b/lib/jedit/isabelle.xml	Thu Feb 28 17:33:35 2008 +0100
@@ -323,6 +323,7 @@
       <INVALID>undo</INVALID>
       <INVALID>undos_proof</INVALID>
       <OPERATOR>unfolding</OPERATOR>
+      <LABEL>unused_thms</LABEL>
       <LABEL>use</LABEL>
       <LABEL>use_thy</LABEL>
       <KEYWORD4>uses</KEYWORD4>
diff -r 0cc3ff184282 -r 64ee6a2ca6d6 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Feb 28 16:54:56 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Feb 28 17:33:35 2008 +0100
@@ -94,6 +94,8 @@
   val thm_deps: (thmref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
   val find_theorems: (int option * bool) * (bool * string FindTheorems.criterion) list
     -> Toplevel.transition -> Toplevel.transition
+  val unused_thms: (string list * string list option) option ->
+    Toplevel.transition -> Toplevel.transition
   val print_binds: Toplevel.transition -> Toplevel.transition
   val print_cases: Toplevel.transition -> Toplevel.transition
   val print_stmts: string list * (thmref * Attrib.src list) list
@@ -531,6 +533,28 @@
   in FindTheorems.print_theorems ctxt opt_goal opt_lim rem_dups spec end);
 
 
+(* find unused theorems *)
+
+local
+
+fun pretty_name_thm (a, th) =
+  Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, Display.pretty_thm th];
+
+in
+
+fun unused_thms opt_range =
+  Toplevel.keep (fn state => ThmDeps.unused_thms
+    (case opt_range of
+       NONE => (NONE, [Toplevel.theory_of state])
+     | SOME (xs, NONE) =>
+         (SOME (map ThyInfo.get_theory xs), [Toplevel.theory_of state])
+     | SOME (xs, SOME ys) =>
+        (SOME (map ThyInfo.get_theory xs), map ThyInfo.get_theory ys)) |>
+           map pretty_name_thm |> Pretty.chunks |> Pretty.writeln);
+
+end;        
+
+
 (* print proof context contents *)
 
 val print_binds = Toplevel.unknown_context o Toplevel.keep (fn state =>
diff -r 0cc3ff184282 -r 64ee6a2ca6d6 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Feb 28 16:54:56 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Feb 28 17:33:35 2008 +0100
@@ -924,6 +924,12 @@
       (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
         (Code.print_codesetup o Toplevel.theory_of)));
 
+val _ =
+  OuterSyntax.improper_command "unused_thms" "find unused theorems" K.diag
+    (Scan.option ((Scan.repeat1 (Scan.unless P.minus P.name) --| P.minus) --
+       Scan.option (Scan.repeat1 (Scan.unless P.minus P.name))) >>
+         (Toplevel.no_timing oo IsarCmd.unused_thms));
+
 
 (** system commands (for interactive mode only) **)