# HG changeset patch
# User blanchet
# Date 1379922486 -7200
# Node ID 298774dbdde0b180caafb55612574014a9848237
# Parent  8d9f4e89d8c8678fe25d244431138c753af1e071
provide a way to override MaSh's port from configuration file

diff -r 8d9f4e89d8c8 -r 298774dbdde0 src/HOL/Tools/Sledgehammer/MaSh/etc/settings
--- a/src/HOL/Tools/Sledgehammer/MaSh/etc/settings	Mon Sep 23 09:08:07 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/MaSh/etc/settings	Mon Sep 23 09:48:06 2013 +0200
@@ -1,3 +1,6 @@
 # -*- shell-script -*- :mode=shellscript:
 
 ISABELLE_SLEDGEHAMMER_MASH="$COMPONENT"
+
+# MASH=yes
+MASH_PORT=9255
diff -r 8d9f4e89d8c8 -r 298774dbdde0 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Sep 23 09:08:07 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Sep 23 09:48:06 2013 +0200
@@ -163,14 +163,17 @@
     val cmd_file = temp_dir ^ "/mash_commands" ^ serial
     val cmd_path = Path.explode cmd_file
     val model_dir = File.shell_path (mash_model_dir ())
-    val core = "--inputFile " ^ cmd_file ^ " --predictions " ^ sugg_file
     val command =
       "cd \"$ISABELLE_SLEDGEHAMMER_MASH\"/src; \
-      \PYTHONDONTWRITEBYTECODE=y ./mash.py --quiet\
+      \PYTHONDONTWRITEBYTECODE=y ./mash.py\
+      \ --quiet\
+      \ --port=$MASH_PORT\
       \ --outputDir " ^ model_dir ^
       " --modelFile=" ^ model_dir ^ "/model.pickle\
       \ --dictsFile=" ^ model_dir ^ "/dict.pickle\
-      \ --log " ^ log_file ^ " " ^ core ^
+      \ --log " ^ log_file ^
+      " --inputFile " ^ cmd_file ^
+      " --predictions " ^ sugg_file ^
       (if extra_args = [] then "" else " " ^ space_implode " " extra_args) ^
       " >& " ^ err_file ^
       (if background then " &" else "")