equal
deleted
inserted
replaced
773 val ord = effective_term_order ctxt name |
773 val ord = effective_term_order ctxt name |
774 val full_proof = debug orelse isar_proof |
774 val full_proof = debug orelse isar_proof |
775 val args = arguments ctxt full_proof extra slice_timeout |
775 val args = arguments ctxt full_proof extra slice_timeout |
776 (ord, ord_info, sel_weights) |
776 (ord, ord_info, sel_weights) |
777 val command = |
777 val command = |
778 File.shell_path command0 ^ " " ^ args ^ " " ^ |
778 "(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ |
779 File.shell_path prob_file |
779 File.shell_path prob_file ^ ")" |
780 |> enclose "TIMEFORMAT='%3R'; { time " " ; } 2>&1" |
780 |> enclose "TIMEFORMAT='%3R'; { time " " ; }" |
781 val _ = |
781 val _ = |
782 atp_problem |
782 atp_problem |
783 |> lines_for_atp_problem format ord ord_info |
783 |> lines_for_atp_problem format ord ord_info |
784 |> cons ("% " ^ command ^ "\n") |
784 |> cons ("% " ^ command ^ "\n") |
785 |> File.write_list prob_file |
785 |> File.write_list prob_file |