# HG changeset patch
# User blanchet
# Date 1410177388 -7200
# Node ID 3e22d3ed829f6f650bf83ecda6910bae7192eafe
# Parent  369513534627556d92a86c307066aaa1229cfecb
refactored MaSh files to avoid regenerating exports on each eval

diff -r 369513534627 -r 3e22d3ed829f src/HOL/TPTP/MaSh_Eval.thy
--- a/src/HOL/TPTP/MaSh_Eval.thy	Mon Sep 08 13:56:27 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Eval.thy	Mon Sep 08 13:56:28 2014 +0200
@@ -5,7 +5,7 @@
 header {* MaSh Evaluation Driver *}
 
 theory MaSh_Eval
-imports MaSh_Export
+imports MaSh_Export_Base
 begin
 
 ML_file "mash_eval.ML"
@@ -23,11 +23,7 @@
 *}
 
 ML {*
-val do_it = false (* switch to "true" to generate the files *)
 val params = Sledgehammer_Commands.default_params @{theory} []
-val range = (1, NONE)
-val dir = "List"
-val prefix = "/tmp/" ^ dir ^ "/"
 val prob_dir = prefix ^ "mash_problems"
 *}
 
diff -r 369513534627 -r 3e22d3ed829f src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Mon Sep 08 13:56:27 2014 +0200
+++ b/src/HOL/TPTP/MaSh_Export.thy	Mon Sep 08 13:56:28 2014 +0200
@@ -5,40 +5,9 @@
 header {* MaSh Exporter *}
 
 theory MaSh_Export
-imports Main
+imports MaSh_Export_Base
 begin
 
-ML_file "mash_export.ML"
-
-sledgehammer_params
-  [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
-   lam_trans = lifting, timeout = 2, dont_preplay, minimize]
-
-declare [[sledgehammer_fact_duplicates = true]]
-declare [[sledgehammer_instantiate_inducts = false]]
-
-hide_fact (open) HOL.ext
-
-ML {*
-Multithreading.max_threads_value ()
-*}
-
-ML {*
-open MaSh_Export
-*}
-
-ML {*
-val do_it = false (* switch to "true" to generate the files *)
-val thys = [@{theory List}]
-val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
-val prover = hd provers
-val range = (1, NONE)
-val step = 1
-val max_suggestions = 1024
-val dir = "List"
-val prefix = "/tmp/" ^ dir ^ "/"
-*}
-
 ML {*
 if do_it then
   Isabelle_System.mkdir (Path.explode prefix)
diff -r 369513534627 -r 3e22d3ed829f src/HOL/TPTP/MaSh_Export_Base.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TPTP/MaSh_Export_Base.thy	Mon Sep 08 13:56:28 2014 +0200
@@ -0,0 +1,42 @@
+(*  Title:      HOL/TPTP/MaSh_Export_Base.thy
+    Author:     Jasmin Blanchette, TU Muenchen
+*)
+
+header {* MaSh Exporter Base *}
+
+theory MaSh_Export_Base
+imports Main
+begin
+
+ML_file "mash_export.ML"
+
+sledgehammer_params
+  [provers = spass, max_facts = 32, strict, dont_slice, type_enc = mono_native,
+   lam_trans = lifting, timeout = 2, dont_preplay, minimize]
+
+declare [[sledgehammer_fact_duplicates = true]]
+declare [[sledgehammer_instantiate_inducts = false]]
+
+hide_fact (open) HOL.ext
+
+ML {*
+Multithreading.max_threads_value ()
+*}
+
+ML {*
+open MaSh_Export
+*}
+
+ML {*
+val do_it = false (* switch to "true" to generate the files *)
+val thys = [@{theory List}]
+val params as {provers, ...} = Sledgehammer_Commands.default_params @{theory} []
+val prover = hd provers
+val range = (1, NONE)
+val step = 1
+val max_suggestions = 1024
+val dir = "List"
+val prefix = "/tmp/" ^ dir ^ "/"
+*}
+
+end