equal
deleted
inserted
replaced
61 val command = |
61 val command = |
62 File.shell_path (Path.explode path) ^ " " ^ |
62 File.shell_path (Path.explode path) ^ " " ^ |
63 arguments ctxt false "" atp_timeout (File.shell_path prob_file) |
63 arguments ctxt false "" atp_timeout (File.shell_path prob_file) |
64 (ord, K [], K []) |
64 (ord, K [], K []) |
65 val outcome = |
65 val outcome = |
66 TimeLimit.timeLimit atp_timeout Isabelle_System.bash_output command |
66 Timeout.apply atp_timeout Isabelle_System.bash_output command |
67 |> fst |
67 |> fst |
68 |> extract_tstplike_proof_and_outcome false proof_delims known_failures |
68 |> extract_tstplike_proof_and_outcome false proof_delims known_failures |
69 |> snd |
69 |> snd |
70 handle TimeLimit.TimeOut => SOME TimedOut |
70 handle Timeout.TIMEOUT _ => SOME TimedOut |
71 val _ = |
71 val _ = |
72 tracing ("Ran ATP: " ^ |
72 tracing ("Ran ATP: " ^ |
73 (case outcome of |
73 (case outcome of |
74 NONE => "Success" |
74 NONE => "Success" |
75 | SOME failure => string_of_atp_failure failure)) |
75 | SOME failure => string_of_atp_failure failure)) |