Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
catch all parsing errors
authorblanchet
Tue, 18 Dec 2012 02:18:45 +0100
changeset 50590 9d2f223ab6d9
parent 50589 42f3630a6a0f
child 50591 c5e0073558f3
catch all parsing errors
src/HOL/Tools/ATP/atp_proof.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Dec 18 00:17:37 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Dec 18 02:18:45 2012 +0100
@@ -496,13 +496,13 @@
 fun parse_line problem =
   parse_tstp_line problem || parse_spass_line || parse_z3_tptp_line
   || parse_satallax_line
-fun parse_proof problem tstp =
-  tstp |> strip_spaces_except_between_idents
-       |> raw_explode
-       |> Scan.finite Symbol.stopper
-              (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
-                              (Scan.repeat1 (parse_line problem))))
-       |> fst
+fun parse_proof problem =
+  strip_spaces_except_between_idents
+  #> raw_explode
+  #> Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
+         (Scan.finite Symbol.stopper
+                         (Scan.repeat1 (parse_line problem))))
+  #> fst
 
 fun atp_proof_from_tstplike_proof _ "" = []
   | atp_proof_from_tstplike_proof problem tstp =
isabelle