# HG changeset patch
# User paulson
# Date 1145436233 -7200
# Node ID b07e3bca20c94defb9cdb5dbdf5445f32af28a33
# Parent  72dab71cb11e5d93f7bef2bf4bb8c2e23de37ca6
fix to spacing in switches, for Vampire under SML/NJ

diff -r 72dab71cb11e -r b07e3bca20c9 src/HOL/Tools/ATP/watcher.ML
--- a/src/HOL/Tools/ATP/watcher.ML	Wed Apr 19 10:43:09 2006 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML	Wed Apr 19 10:43:53 2006 +0200
@@ -195,12 +195,16 @@
              error "")
     | numbers => valOf (Int.fromString (List.last numbers));
 
-(* call ATP.  Settings should be a list of strings  ["-t300", "-m100000"]*)
+(*Call ATP.  Settings should be a list of strings  ["-t 300", "-m 100000"],
+  which we convert below to ["-t", "300", "-m", "100000"] using String.tokens.
+  Otherwise, the SML/NJ version of Unix.execute will escape the spaces, and
+  Vampire will reject the switches.*)
 fun execCmds [] procList = procList
   | execCmds ((prover,proverCmd,settings,file)::cmds) procList  =
       let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ file)
+          val settings' = List.concat (map (String.tokens Char.isSpace) settings)
 	  val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
-	       Unix.execute(proverCmd, settings@[file])
+	       Unix.execute(proverCmd, settings' @ [file])
 	  val (instr, outstr) = Unix.streamsOf childhandle
 	  val newProcList = {prover=prover, file=file, proc_handle=childhandle,
 			     instr=instr, outstr=outstr} :: procList