# HG changeset patch # User wenzelm # Date 1117963883 -7200 # Node ID 4a1f36eafe17e681fc509b464319c240e63f3aff # Parent aed1a8ae4b239ee6376ab27a26e57553cefc1fd2 File.platform_path vs. File.shell_path; diff -r aed1a8ae4b23 -r 4a1f36eafe17 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Sun Jun 05 11:31:22 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Sun Jun 05 11:31:23 2005 +0200 @@ -168,19 +168,19 @@ (*** only include problem and clasimp for the moment, not sure how to refer to ***) (*** hyps/local axioms just now (*,axfile, hypsfile,*) ***) - val whole_prob_file = system ("/bin/cat " ^ clasimpfile ^" "^ probfile ^ " > " ^ (File.sysify_path wholefile)) + val whole_prob_file = system ("cat " ^ clasimpfile ^" "^ probfile ^ " > " ^ File.shell_path wholefile) val dfg_create = if File.exists dfg_dir then warning("dfg dir exists") else File.mkdir dfg_dir; - val dfg_path = File.sysify_path dfg_dir; + val dfg_path = File.platform_path dfg_dir; (* val exec_tptp2x = Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X", - ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile]) *) + ["-fdfg", "-d " ^ dfg_path, File.platform_path wholefile]) *) val tptp_home = getenv "TPTP2X_HOME" ^ "/tptp2X" - val systemcall = system (tptp_home^" -fdfg -d " ^ dfg_path^" "^( File.sysify_path wholefile)) + val systemcall = system (tptp_home ^ " -fdfg -d " ^ File.shell_path dfg_dir ^ " " ^ File.shell_path wholefile) val _ = warning("systemcall is "^ (string_of_int systemcall)) (*val _ = Posix.Process.wait ()*) (*val _ =Unix.reap exec_tptp2x*) @@ -191,7 +191,7 @@ Posix.Process.sleep(Time.fromSeconds 1); (warning ("probfile is: "^probfile)); (warning("dfg file is: "^newfile)); - (warning ("wholefile is: "^(File.sysify_path wholefile))); + (warning ("wholefile is: "^(File.platform_path wholefile))); sendOutput (toWatcherStr, prover ^ "*" ^ thmstring ^ "*" ^ goalstring ^ "*" ^ proverCmd ^ "*" ^ settings ^ "*" ^ newfile ^ "\n"); @@ -202,7 +202,7 @@ (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg"))) then callResProvers (toWatcherStr, args) else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^ - " -fdfg " ^ File.sysify_path wholefile ^ " -d " ^ dfg_path) + " -fdfg " ^ File.platform_path wholefile ^ " -d " ^ dfg_path) end (* fun callResProversStr (toWatcherStr, []) = "End of calls\n" @@ -369,7 +369,7 @@ val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) ) *) (*val goalstr = string_of_thm (the_goal) - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher"))); + val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher"))); val _ = TextIO.output (outfile,goalstr ) val _ = TextIO.closeOut outfile*) fun killChildren [] = () @@ -722,11 +722,11 @@ fun spass_proofHandler (n) = ( - let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1"))); + let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_signal1"))); val _ = TextIO.output (outfile, ("In signal handler now\n")) val _ = TextIO.closeOut outfile val (reconstr, thmstring, goalstring) = SpassComm.getSpassInput childin - val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_signal"))); + val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal"))); val _ = TextIO.output (outfile, ("In signal handler "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))) val _ = TextIO.closeOut outfile @@ -743,7 +743,7 @@ if ((!goals_being_watched) = 0) then - (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_found"))); + (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_found"))); val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) val _ = TextIO.closeOut outfile in @@ -762,7 +762,7 @@ Pretty.writeln(Pretty.str (oct_char "361")); if (!goals_being_watched = 0) then - (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp"))); + (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp"))); val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) val _ = TextIO.closeOut outfile in @@ -781,7 +781,7 @@ Pretty.writeln(Pretty.str (oct_char "361")); if (!goals_being_watched = 0) then - (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp"))); + (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp"))); val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) val _ = TextIO.closeOut outfile in @@ -801,7 +801,7 @@ Pretty.writeln(Pretty.str (oct_char "361")); if (!goals_being_watched = 0) then - (let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp"))); + (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp"))); val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) val _ = TextIO.closeOut outfile in