# HG changeset patch
# User desharna
# Date 1648629458 -7200
# Node ID 48736d743e8c98ae8c7aaa21c89325e632cad96c
# Parent  4c8d1ef258d353632aedbcb4c69f542dee12d542
expanded sledgehammer's expect option with some_preplayed

diff -r 4c8d1ef258d3 -r 48736d743e8c src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Mar 29 17:12:15 2022 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Mar 30 10:37:38 2022 +0200
@@ -246,11 +246,20 @@
   in
     (* The "expect" argument is deliberately ignored if the prover is missing so that
        "Metis_Examples" can be processed on any machine. *)
-    if expect = "" orelse outcome_code = expect orelse
-       not (is_prover_installed ctxt prover_name) then
+    if expect = "" orelse not (is_prover_installed ctxt prover_name) then
       ()
     else
-      error ("Unexpected outcome: " ^ quote outcome_code)
+      (case (expect, outcome) of
+        ("some", SH_Some _) => ()
+      | ("some_preplayed", SH_Some (_, preplay_results)) =>
+          if exists (fn (_, Played _, _) => true | _ => false) preplay_results then
+            ()
+          else
+            error ("Unexpected outcome: the external prover found a some proof but preplay failed")
+      | ("unknown", SH_Unknown) => ()
+      | ("timeout", SH_Timeout) => ()
+      | ("none", SH_None) => ()
+      | _ => error ("Unexpected outcome: " ^ quote outcome_code))
   end
 
 fun launch_prover_and_preplay (params as {debug, timeout, expect, ...}) mode writeln_result learn