# HG changeset patch
# User blanchet
# Date 1377069940 -7200
# Node ID 43d5f3d6d04e467169748482d742cc7bc961c5d7
# Parent  ac18480cbf9d6d573c6921da427dfdf41ac114c9
generate max suggestions in MaSh export driver

diff -r ac18480cbf9d -r 43d5f3d6d04e src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Wed Aug 21 09:25:40 2013 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Aug 21 09:25:40 2013 +0200
@@ -71,16 +71,16 @@
 
 ML {*
 if do_it then
-  generate_isar_commands @{context} prover (range, step) thys
-      linearize (prefix ^ "mash_commands")
+  generate_isar_commands @{context} prover (range, step) thys linearize
+      max_suggestions (prefix ^ "mash_commands")
 else
   ()
 *}
 
 ML {*
 if do_it then
-  generate_mepo_suggestions @{context} params (range, step) thys
-      linearize max_suggestions (prefix ^ "mepo_suggestions")
+  generate_mepo_suggestions @{context} params (range, step) thys linearize
+      max_suggestions (prefix ^ "mepo_suggestions")
 else
   ()
 *}
@@ -103,8 +103,8 @@
 
 ML {*
 if do_it then
-  generate_prover_commands @{context} params (range, step) thys
-      linearize (prefix ^ "mash_prover_commands")
+  generate_prover_commands @{context} params (range, step) thys linearize
+      max_suggestions (prefix ^ "mash_prover_commands")
 else
   ()
 *}
diff -r ac18480cbf9d -r 43d5f3d6d04e src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Wed Aug 21 09:25:40 2013 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Wed Aug 21 09:25:40 2013 +0200
@@ -20,10 +20,10 @@
     -> unit
   val generate_isar_commands :
     Proof.context -> string -> (int * int option) * int -> theory list -> bool
-    -> string -> unit
+    -> int -> string -> unit
   val generate_prover_commands :
     Proof.context -> params -> (int * int option) * int -> theory list -> bool
-    -> string -> unit
+    -> int -> string -> unit
   val generate_mepo_suggestions :
     Proof.context -> params -> (int * int option) * int -> theory list -> bool
     -> int -> string -> unit
@@ -146,7 +146,7 @@
   is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
 
 fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys
-                                     linearize file_name =
+                                     linearize max_suggs file_name =
   let
     val ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover
     val path = file_name |> Path.explode
@@ -172,7 +172,7 @@
             encode_features (sort_wrt fst feats)
           val query =
             if is_bad_query ctxt ho_atp step j th isar_deps then ""
-            else "? " ^ core ^ "\n"
+            else "? " ^ string_of_int max_suggs ^ " # " ^ core ^ "\n"
           val update =
             "! " ^ core ^ "; " ^ marker ^ " " ^ encode_strs deps ^ "\n"
         in query ^ update end