# HG changeset patch
# User blanchet
# Date 1284500183 -7200
# Node ID 4b35206e63609c93691f499d53d617a6bfcfef59
# Parent  fe95c860434c5cacba8c12efbeb7c80dc88baa38
fix splitting of proof lines for one-line metis calls;
needed for newly supported ATPs (Vampire 0.6 local and remote, SNARK)

diff -r fe95c860434c -r 4b35206e6360 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Sep 14 23:01:29 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Sep 14 23:36:23 2010 +0200
@@ -71,7 +71,10 @@
 
 fun raw_step_name_ord p =
   let val q = pairself raw_step_num p in
-    case pairself Int.fromString q of
+    (* The "unprefix" part is to cope with remote Vampire's output. The proper
+       solution would be to perform a topological sort, e.g. using the nice
+       "Graph" functor. *)
+    case pairself (Int.fromString o perhaps (try (unprefix "f"))) q of
       (NONE, NONE) => string_ord q
     | (NONE, SOME _) => LESS
     | (SOME _, NONE) => GREATER
@@ -604,14 +607,14 @@
 
 (** EXTRACTING LEMMAS **)
 
-(* Like "split_line", but ignores "\n" that follow a comma (as in SNARK's
-   output). *)
+(* Like "split_line" but splits on ".\n" (for TSTP and SPASS) or "]\n" (for
+   Vampire). *)
 val split_proof_lines =
   let
     fun aux [] [] = []
       | aux line [] = [implode (rev line)]
-      | aux line ("," :: "\n" :: rest) = aux ("," :: line) rest
-      | aux line ("\n" :: rest) = aux line [] @ aux [] rest
+      | aux line ("." :: "\n" :: rest) = aux line [] @ aux [] rest
+      | aux line ("]" :: "\n" :: rest) = aux line [] @ aux [] rest
       | aux line (s :: rest) = aux (s :: line) rest
   in aux [] o explode end