# HG changeset patch
# User haftmann
# Date 1475498071 -7200
# Node ID 048b7dbfdfa36d7c0d03fbd46e02903781d0be3c
# Parent  789f5419926a115933236ff363f91d2f00ce0c17
option to report results of solve_direct as explicit warnings

diff -r 789f5419926a -r 048b7dbfdfa3 NEWS
--- a/NEWS	Mon Oct 03 14:34:30 2016 +0200
+++ b/NEWS	Mon Oct 03 14:34:31 2016 +0200
@@ -60,6 +60,9 @@
     introduction and elimination rules after each split rule. As a
     result the subgoal may be split into several subgoals.
 
+* Solve direct: option 'solve_direct_strict_warnings' gives explicit
+  warnings for lemma statements with trivial proofs.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
diff -r 789f5419926a -r 048b7dbfdfa3 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Mon Oct 03 14:34:30 2016 +0200
+++ b/src/Tools/solve_direct.ML	Mon Oct 03 14:34:31 2016 +0200
@@ -15,6 +15,7 @@
   val noneN: string
   val unknownN: string
   val max_solutions: int Config.T
+  val strict_warnings: bool Config.T
   val solve_direct: Proof.state -> bool * (string * string list)
 end;
 
@@ -33,6 +34,7 @@
 (* preferences *)
 
 val max_solutions = Attrib.setup_config_int @{binding solve_direct_max_solutions} (K 5);
+val strict_warnings = Attrib.setup_config_bool @{binding solve_direct_strict_warnings} (K false);
 
 
 (* solve_direct command *)
@@ -77,8 +79,15 @@
     (case try seek_against_goal () of
       SOME (SOME results) =>
         (someN,
-          let val msg = Pretty.string_of (Pretty.chunks (message results))
-          in if mode = Auto_Try then [msg] else (writeln msg; []) end)
+          let
+            val msg = Pretty.string_of (Pretty.chunks (message results))
+          in
+            if Config.get ctxt strict_warnings
+            then (warning msg; [])
+            else if mode = Auto_Try
+              then [msg]
+              else (writeln msg; [])
+          end)
     | SOME NONE =>
         (if mode = Normal then writeln "No proof found"
          else ();