# HG changeset patch
# User blanchet
# Date 1402940502 -7200
# Node ID 6a3b5085fb8fd39265eeddab94719facdb1ea227
# Parent  cab38f7a3adb2ba4b714a0eeea7ed4c14fc0baa3
fixed parsing of one-argument 'file()' in TSTP files

diff -r cab38f7a3adb -r 6a3b5085fb8f src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Mon Jun 16 19:41:01 2014 +0200
+++ b/src/HOL/Sledgehammer.thy	Mon Jun 16 19:41:42 2014 +0200
@@ -33,8 +33,4 @@
 ML_file "Tools/Sledgehammer/sledgehammer.ML"
 ML_file "Tools/Sledgehammer/sledgehammer_commands.ML"
 
-lemma "1 + 1 = (2::nat)"
-sledgehammer [remote_waldmeister, max_facts = 3, verbose, overlord]
-oops
-
 end
diff -r cab38f7a3adb -r 6a3b5085fb8f src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 16 19:41:01 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Jun 16 19:41:42 2014 +0200
@@ -21,6 +21,7 @@
     GaveUp |
     ProofMissing |
     ProofIncomplete |
+    ProofUnparsable |
     UnsoundProof of bool * string list |
     CantConnect |
     TimedOut |
@@ -132,6 +133,7 @@
   GaveUp |
   ProofMissing |
   ProofIncomplete |
+  ProofUnparsable |
   UnsoundProof of bool * string list |
   CantConnect |
   TimedOut |
@@ -164,8 +166,9 @@
   | string_of_atp_failure ProofMissing =
     "The prover claims the conjecture is a theorem but did not provide a proof."
   | string_of_atp_failure ProofIncomplete =
-    "The prover claims the conjecture is a theorem but provided an incomplete \
-    \(or unparsable) proof."
+    "The prover claims the conjecture is a theorem but provided an incomplete proof."
+  | string_of_atp_failure ProofUnparsable =
+    "The prover claims the conjecture is a theorem but provided an unparsable proof."
   | string_of_atp_failure (UnsoundProof (false, ss)) =
     "The prover derived \"False\"" ^ from_lemmas ss ^
     ". Specify a sound type encoding or omit the \"type_enc\" option."
@@ -234,6 +237,7 @@
   (case (extract_tstplike_proof proof_delims output,
       extract_known_atp_failure known_failures output) of
     (_, SOME ProofIncomplete) => ("", NONE)
+  | (_, SOME ProofUnparsable) => ("", NONE)
   | ("", SOME ProofMissing) => ("", NONE)
   | ("", NONE) => ("", SOME (UnknownError (short_output verbose output)))
   | res as ("", _) => res
@@ -300,7 +304,7 @@
 and parse_file_source x =
   (Scan.this_string "file" |-- $$ "(" |-- scan_general_id
    -- Scan.option ($$ "," |-- scan_general_id
-  --| Scan.option ($$"," |-- $$"[" -- Scan.option scan_general_id --| $$"]") --| $$ ")")) x
+     --| Scan.option ($$ "," |-- $$ "[" -- Scan.option scan_general_id --| $$ "]")) --| $$ ")") x
 and parse_inference_source x =
   (Scan.this_string "inference" |-- $$ "(" |-- scan_general_id
    --| skip_term --| $$ "," --| skip_term --| $$ "," --| $$ "["
diff -r cab38f7a3adb -r 6a3b5085fb8f src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Jun 16 19:41:01 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Jun 16 19:41:42 2014 +0200
@@ -290,7 +290,7 @@
                      (accum,
                       extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
                       |>> atp_proof_of_tstplike_proof (perhaps (try (unprefix remote_prefix)) name) atp_problem
-                      handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
+                      handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofUnparsable)))
               handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut))
 
             val outcome =