catch all parsing errors
authorblanchet
Tue Dec 18 02:18:45 2012 +0100 (2012-12-18)
changeset 505909d2f223ab6d9
parent 50589 42f3630a6a0f
child 50591 c5e0073558f3
catch all parsing errors
src/HOL/Tools/ATP/atp_proof.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Dec 18 00:17:37 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Dec 18 02:18:45 2012 +0100
     1.3 @@ -496,13 +496,13 @@
     1.4  fun parse_line problem =
     1.5    parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line
     1.6    || parse_satallax_line
     1.7 -fun parse_proof problem tstp =
     1.8 -  tstp |> strip_spaces_except_between_idents
     1.9 -       |> raw_explode
    1.10 -       |> Scan.finite Symbol.stopper
    1.11 -              (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
    1.12 -                              (Scan.repeat1 (parse_line problem))))
    1.13 -       |> fst
    1.14 +fun parse_proof problem =
    1.15 +  strip_spaces_except_between_idents
    1.16 +  #> raw_explode
    1.17 +  #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
    1.18 +         (Scan.finite Symbol.stopper
    1.19 +                         (Scan.repeat1 (parse_line problem))))
    1.20 +  #> fst
    1.21  
    1.22  fun atp_proof_from_tstplike_proof _ "" = []
    1.23    | atp_proof_from_tstplike_proof problem tstp =