option to report results of solve_direct as explicit warnings
authorhaftmann
Mon Oct 03 14:34:31 2016 +0200 (2016-10-03)
changeset 64013048b7dbfdfa3
parent 64012 789f5419926a
child 64014 ca1239a3277b
option to report results of solve_direct as explicit warnings
NEWS
src/Tools/solve_direct.ML
     1.1 --- a/NEWS	Mon Oct 03 14:34:30 2016 +0200
     1.2 +++ b/NEWS	Mon Oct 03 14:34:31 2016 +0200
     1.3 @@ -60,6 +60,9 @@
     1.4      introduction and elimination rules after each split rule. As a
     1.5      result the subgoal may be split into several subgoals.
     1.6  
     1.7 +* Solve direct: option 'solve_direct_strict_warnings' gives explicit
     1.8 +  warnings for lemma statements with trivial proofs.
     1.9 +
    1.10  
    1.11  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.12  
     2.1 --- a/src/Tools/solve_direct.ML	Mon Oct 03 14:34:30 2016 +0200
     2.2 +++ b/src/Tools/solve_direct.ML	Mon Oct 03 14:34:31 2016 +0200
     2.3 @@ -15,6 +15,7 @@
     2.4    val noneN: string
     2.5    val unknownN: string
     2.6    val max_solutions: int Config.T
     2.7 +  val strict_warnings: bool Config.T
     2.8    val solve_direct: Proof.state -> bool * (string * string list)
     2.9  end;
    2.10  
    2.11 @@ -33,6 +34,7 @@
    2.12  (* preferences *)
    2.13  
    2.14  val max_solutions = Attrib.setup_config_int @{binding solve_direct_max_solutions} (K 5);
    2.15 +val strict_warnings = Attrib.setup_config_bool @{binding solve_direct_strict_warnings} (K false);
    2.16  
    2.17  
    2.18  (* solve_direct command *)
    2.19 @@ -77,8 +79,15 @@
    2.20      (case try seek_against_goal () of
    2.21        SOME (SOME results) =>
    2.22          (someN,
    2.23 -          let val msg = Pretty.string_of (Pretty.chunks (message results))
    2.24 -          in if mode = Auto_Try then [msg] else (writeln msg; []) end)
    2.25 +          let
    2.26 +            val msg = Pretty.string_of (Pretty.chunks (message results))
    2.27 +          in
    2.28 +            if Config.get ctxt strict_warnings
    2.29 +            then (warning msg; [])
    2.30 +            else if mode = Auto_Try
    2.31 +              then [msg]
    2.32 +              else (writeln msg; [])
    2.33 +          end)
    2.34      | SOME NONE =>
    2.35          (if mode = Normal then writeln "No proof found"
    2.36           else ();