equal
deleted
inserted
replaced
119 val qf = File.shell_path and qq = enclose "'" "'" |
119 val qf = File.shell_path and qq = enclose "'" "'" |
120 val path = getenv env_var and remote = getenv "REMOTE_SMT_SOLVER" |
120 val path = getenv env_var and remote = getenv "REMOTE_SMT_SOLVER" |
121 fun cmd f1 f2 = |
121 fun cmd f1 f2 = |
122 if path <> "" |
122 if path <> "" |
123 then map qq (path :: args) @ [qf f1, ">", qf f2] |
123 then map qq (path :: args) @ [qf f1, ">", qf f2] |
124 else map qq (remote :: remote_name :: args) @ [qf f1, qf f2] |
124 else "perl -w" :: map qq (remote :: remote_name :: args) @ [qf f1, qf f2] |
125 in with_tmp_files run (ctxt, space_implode " " oo cmd, output) end |
125 in with_tmp_files run (ctxt, space_implode " " oo cmd, output) end |
126 |
126 |
127 end |
127 end |
128 |
128 |
129 fun make_proof_data ctxt ((recon, thms), ls) = |
129 fun make_proof_data ctxt ((recon, thms), ls) = |