# HG changeset patch
# User blanchet
# Date 1360322557 -3600
# Node ID 69da236d78387766746b2510aa789b0d14338a1f
# Parent  63d71b24732385dff6b087e4fa1b436ab333c6a5
added option to use SNoW as machine learning algo

diff -r 63d71b247323 -r 69da236d7838 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Feb 07 18:39:24 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Feb 08 12:22:37 2013 +0100
@@ -15,6 +15,7 @@
   type prover_result = Sledgehammer_Provers.prover_result
 
   val trace : bool Config.T
+  val snow : bool Config.T
   val MePoN : string
   val MaShN : string
   val MeShN : string
@@ -106,6 +107,9 @@
 
 val trace =
   Attrib.setup_config_bool @{binding sledgehammer_mash_trace} (K false)
+val snow =
+  Attrib.setup_config_bool @{binding sledgehammer_mash_snow} (K false)
+
 fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
 
 val MePoN = "MePo"
@@ -157,7 +161,9 @@
       " --numberOfPredictions " ^ string_of_int max_suggs ^
       (* " --learnTheories" ^ *) (if save then " --saveModel" else "")
     val command =
-      "\"$ISABELLE_SLEDGEHAMMER_MASH/src/mash.py\" --quiet" ^
+      "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; " ^
+      "./mash.py --quiet" ^
+      (if Config.get ctxt snow then " --snow" else "") ^
       " --outputDir " ^ model_dir ^
       " --modelFile=" ^ model_dir ^ "/model.pickle" ^
       " --dictsFile=" ^ model_dir ^ "/dict.pickle" ^