equal
deleted
inserted
replaced
89 MalformedOutput | |
89 MalformedOutput | |
90 Interrupted | |
90 Interrupted | |
91 Crashed | |
91 Crashed | |
92 InternalError | |
92 InternalError | |
93 UnknownError of string |
93 UnknownError of string |
94 |
|
95 fun is_ident_char c = Char.isAlphaNum c orelse c = #"_" |
|
96 val strip_spaces_except_between_ident_chars = strip_spaces true is_ident_char |
|
97 |
94 |
98 fun elide_string threshold s = |
95 fun elide_string threshold s = |
99 if size s > threshold then |
96 if size s > threshold then |
100 String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^ |
97 String.extract (s, 0, SOME (threshold div 2 - 5)) ^ " ...... " ^ |
101 String.extract (s, size s - (threshold + 1) div 2 + 6, NONE) |
98 String.extract (s, size s - (threshold + 1) div 2 + 6, NONE) |
473 map (swap o `(resolve_spass_num spass_names)) deps))) x |
470 map (swap o `(resolve_spass_num spass_names)) deps))) x |
474 |
471 |
475 fun parse_line problem spass_names = |
472 fun parse_line problem spass_names = |
476 parse_tstp_line problem || parse_spass_line spass_names |
473 parse_tstp_line problem || parse_spass_line spass_names |
477 fun parse_proof problem spass_names tstp = |
474 fun parse_proof problem spass_names tstp = |
478 tstp |> strip_spaces_except_between_ident_chars |
475 tstp |> strip_spaces_except_between_idents |
479 |> raw_explode |
476 |> raw_explode |
480 |> Scan.finite Symbol.stopper |
477 |> Scan.finite Symbol.stopper |
481 (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) |
478 (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ()) |
482 (Scan.repeat1 (parse_line problem spass_names)))) |
479 (Scan.repeat1 (parse_line problem spass_names)))) |
483 |> fst |
480 |> fst |