# HG changeset patch # User wenzelm # Date 1117965434 -7200 # Node ID 4280d6bbc1bbb68ea3fd5b0d11d297637d016813 # Parent 2c05a7f662a3325ba05adb14de7b8c81fe33d1f9 replaced File.sysify_path by Path.pack; avoid "handle _" (which is not well-defined due to erratic Interrupt exceptions); diff -r 2c05a7f662a3 -r 4280d6bbc1bb src/HOL/Tools/sat_solver.ML --- a/src/HOL/Tools/sat_solver.ML Sun Jun 05 11:31:33 2005 +0200 +++ b/src/HOL/Tools/sat_solver.ML Sun Jun 05 11:57:14 2005 +0200 @@ -526,11 +526,11 @@ val cmd = (getenv "ZCHAFF_HOME") ^ "/zchaff " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath) fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) fun readfn () = SatSolver.parse_std_result_file outpath ("Instance Satisfiable", "", "Instance Unsatisfiable") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (File.sysify_path inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (File.sysify_path outpath)) else () + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else () val result = SatSolver.make_external_solver cmd writefn readfn fm - val _ = (File.rm inpath handle _ => ()) - val _ = (File.rm outpath handle _ => ()) + val _ = try File.rm inpath + val _ = try File.rm outpath in result end @@ -551,11 +551,11 @@ val cmd = (getenv "BERKMIN_HOME") ^ "/" ^ (getenv "BERKMIN_EXE") ^ " " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath) fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) fun readfn () = SatSolver.parse_std_result_file outpath ("Satisfiable !!", "solution =", "UNSATISFIABLE !!") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (File.sysify_path inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (File.sysify_path outpath)) else () + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else () val result = SatSolver.make_external_solver cmd writefn readfn fm - val _ = (File.rm inpath handle _ => ()) - val _ = (File.rm outpath handle _ => ()) + val _ = try File.rm inpath + val _ = try File.rm outpath in result end @@ -576,11 +576,11 @@ val cmd = (getenv "JERUSAT_HOME") ^ "/Jerusat1.3 " ^ (Path.pack inpath) ^ " > " ^ (Path.pack outpath) fun writefn fm = SatSolver.write_dimacs_cnf_file inpath (PropLogic.defcnf fm) fun readfn () = SatSolver.parse_std_result_file outpath ("s SATISFIABLE", "v ", "s UNSATISFIABLE") - val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (File.sysify_path inpath)) else () - val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (File.sysify_path outpath)) else () + val _ = if File.exists inpath then warning ("overwriting existing file " ^ quote (Path.pack inpath)) else () + val _ = if File.exists outpath then warning ("overwriting existing file " ^ quote (Path.pack outpath)) else () val result = SatSolver.make_external_solver cmd writefn readfn fm - val _ = (File.rm inpath handle _ => ()) - val _ = (File.rm outpath handle _ => ()) + val _ = try File.rm inpath + val _ = try File.rm outpath in result end