# HG changeset patch
# User blanchet
# Date 1387470257 -3600
# Node ID a510fc40559c4972d80f3feffd4705c2cbfe9f5b
# Parent  d4a56c8267695a975a1bbf52903cfea8c71b49d7
distinguish not preplayed & timed out

diff -r d4a56c826769 -r a510fc40559c src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Dec 19 17:11:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Dec 19 17:24:17 2013 +0100
@@ -88,8 +88,8 @@
     val (failed, reconstr, ext_time) =
       (case preplay of
         Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
-      | Play_Timed_Out (reconstr, time) =>
-        (false, reconstr, if time = Time.zeroTime then NONE else SOME (true, time))
+      | Not_Played reconstr => (false, reconstr, NONE)
+      | Play_Timed_Out (reconstr, time) => (false, reconstr, SOME (true, time))
       | Play_Failed reconstr => (true, reconstr, NONE))
     val try_line =
       ([], map fst extra)
diff -r d4a56c826769 -r a510fc40559c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 19 17:11:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 19 17:24:17 2013 +0100
@@ -404,7 +404,7 @@
       else List.last reconstrs
   in
     if timeout = Time.zeroTime then
-      Play_Timed_Out (get_preferred reconstrs, Time.zeroTime)
+      Not_Played (get_preferred reconstrs)
     else
       let
         val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
diff -r d4a56c826769 -r a510fc40559c src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Dec 19 17:11:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Dec 19 17:24:17 2013 +0100
@@ -405,7 +405,8 @@
 fun isar_proof_would_be_a_good_idea preplay =
   (case preplay of
     Played (reconstr, _) => reconstr = SMT
-  | Play_Timed_Out _ => false
+  | Not_Played _ => false
+  | Play_Timed_Out _ => true
   | Play_Failed _ => true)
 
 fun proof_text ctxt isar_proofs isar_params num_chained
diff -r d4a56c826769 -r a510fc40559c src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Dec 19 17:11:54 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Dec 19 17:24:17 2013 +0100
@@ -15,6 +15,7 @@
 
   datatype play =
     Played of reconstructor * Time.time |
+    Not_Played of reconstructor |
     Play_Timed_Out of reconstructor * Time.time |
     Play_Failed of reconstructor
 
@@ -35,6 +36,7 @@
 
 datatype play =
   Played of reconstructor * Time.time |
+  Not_Played of reconstructor |
   Play_Timed_Out of reconstructor * Time.time |
   Play_Failed of reconstructor