Be less verbose
authorJoachim Breitner <mail@joachim-breitner.de>
Fri, 19 Dec 2014 11:30:49 +0000 (12:30 +0100)
committerJoachim Breitner <mail@joachim-breitner.de>
Fri, 19 Dec 2014 11:30:49 +0000 (12:30 +0100)
README.md
Where_To_Move_Ex4.thy
where_to_move.ML

index 1ede9e5..3ff390f 100644 (file)
--- a/README.md
+++ b/README.md
@@ -89,10 +89,14 @@ Example use
 If I enter the command `where_to_move` at the end of the theory
 `Where_To_Move_Ex4`, I will be given this somewhat helpful output:
 
-    Theorem Where_To_Move_Ex4.barE2 could be moved to theory "Where_To_Move_Ex2". 
-    Theorem Where_To_Move_Ex4.fooI2 could be moved to theory "Where_To_Move_Ex1". 
-    Theorem Where_To_Move_Ex4.foobar could be moved to theory "Where_To_Move_Ex3". 
-    Theorem Where_To_Move_Ex4.foobar2 is fine where it is
+    Theorem barE2 could be moved to theory "Where_To_Move_Ex2". 
+    Theorem fooI2 could be moved to theory "Where_To_Move_Ex1". 
+    Theorem foobar could be moved to theory "Where_To_Move_Ex3". 
+
+The output did not mention `foobar2`, but if I expliclty ask for it to be
+checked using `where_to_move foobar2` I get
+
+    Theorem foobar2 is fine where it is.
 
 Installation
 ------------
index 783f91d..8ca4f31 100644 (file)
@@ -18,5 +18,6 @@ lemma foobar2: "foo \<and> \<not> bar"
   done
 
 where_to_move
+where_to_move foobar2
 
 end
index 69ba23d..e717c6e 100644 (file)
@@ -74,9 +74,9 @@ fun where_to_move_cmd args_o =
   Toplevel.keep ( fn state =>
     let val ctxt = Toplevel.context_of state
         val this_thy = Toplevel.theory_of state
-        val named_thms = case args_o of
-            SOME args => args |> map (Facts.retrieve (Context.Proof ctxt) (Global_Theory.facts_of this_thy))
-            | NONE => facts_of_theory this_thy
+        val (verbose, named_thms) = case args_o of
+            SOME args => (true, args |> map (Facts.retrieve (Context.Proof ctxt) (Global_Theory.facts_of this_thy)))
+            | NONE =>    (false, facts_of_theory this_thy)
     in named_thms |> map (fn (name, thms) =>
       let val pretty_name = Pretty.mark_str (Proof_Context.markup_extern_fact ctxt name)
       in case better_theory (theories_used_by_thms this_thy thms) this_thy of
@@ -84,11 +84,13 @@ fun where_to_move_cmd args_o =
            [ Pretty.str "Theorem ", pretty_name,
              Pretty.str " could be moved to theory ",
              Pretty.quote (Pretty.str (Context.theory_name thy)), Pretty.str "."
-           ]
+           ] |> Pretty.paragraph |> Pretty.writeln
         | NONE =>
+          if verbose then
            [ Pretty.str "Theorem ", pretty_name,
-             Pretty.str" is fine where it is."]
-      end |> Pretty.paragraph |> Pretty.writeln
+             Pretty.str" is fine where it is."] |> Pretty.paragraph |> Pretty.writeln
+          else ()
+      end
     ) |> K ()
    end
    );