# HG changeset patch
# User sultana
# Date 1334675647 -3600
# Node ID ef2d045203373631c2863649a493816ff0b4eebc
# Parent  9c3acd90063acbfaf6aca266fd4b89abe49921fc
improved exception-handling in tptp;
tuned;

diff -r 9c3acd90063a -r ef2d04520337 src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 17 16:14:07 2012 +0100
@@ -825,21 +825,16 @@
       {cautious = cautious,
        problem_name =
         SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode)
-         file_name))
-      }
-    handle _(*FIXME*) =>
-      {cautious = cautious,
-       problem_name = NONE
-      }
+         file_name))}
   in interpret_file' config [] path_prefix file_name end
 
 fun import_file cautious path_prefix file_name type_map const_map thy =
   let
     val prob_name =
       TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name))
-      handle _(*FIXME*) => TPTP_Problem_Name.Nonstandard (Path.implode file_name)
     val (result, thy') =
       interpret_file cautious path_prefix file_name type_map const_map thy
+  (*FIXME doesn't check if problem has already been interpreted*)
   in TPTP_Data.map (cons ((prob_name, result))) thy' end
 
 val _ =
diff -r 9c3acd90063a -r ef2d04520337 src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML	Tue Apr 17 16:14:07 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML	Tue Apr 17 16:14:07 2012 +0100
@@ -56,7 +56,7 @@
 datatype suffix =
     Problem of
       ((*version*)int *
-      (*size parameter*)int option) *
+       (*size parameter*)int option) *
       (*extension*)string
   | Axiom of
       (*specialisation*)int *
@@ -94,10 +94,10 @@
     (*NOTE there's an ambiguity in the spec: there's no way of knowing if a
     file ending in "rm" used to be "ax" or "p". Here we default to "p".*)
     val ((((prob_domain, prob_number), prob_form), suffix), rest) =
-     Scan.finite Symbol.stopper
-     ((alpha ^^ alpha ^^ alpha) --
-     (numer ^^ numer ^^ numer >> to_int) --
-     lift forms -- (prob_suffix || ax_ending)) str
+      Scan.finite Symbol.stopper
+      ((alpha ^^ alpha ^^ alpha) --
+      (numer ^^ numer ^^ numer >> to_int) --
+      lift forms -- (prob_suffix || ax_ending)) str
 
     fun parse_form str =
       case str of
@@ -115,36 +115,41 @@
          prob_number = prob_number,
          prob_form = parse_form prob_form,
          suffix = suffix}
-      handle _ => Nonstandard str'
     else raise TPTP_PROBLEM_NAME ("Parse error")
   end
+  handle exn =>
+    (*FIXME brittle*)
+    if General.exnName exn = "FAIL" andalso General.exnMessage exn = "FAIL NONE" then
+      (*It's very likely that the scanner failed*)
+      Nonstandard str'
+    else reraise exn
 
 (*Produces an ASCII encoding of a TPTP problem-file name.*)
 fun mangle_problem_name (prob : problem_name) : string =
   case prob of
-     Standard tptp_prob =>
-       let
-         val prob_form =
-           case #prob_form tptp_prob of
-             TPTP_Syntax.THF => "_thf_"
-           | TPTP_Syntax.TFF => "_tff_"
-           | TPTP_Syntax.TFF_with_arithmetic => "_thfwa_"
-           | TPTP_Syntax.FOF => "_fof_"
-           | TPTP_Syntax.CNF => "_cnf_"
-         val suffix =
-           case #suffix tptp_prob of
-             Problem ((version, size), extension) =>
-               Int.toString version ^ "_" ^
-               (if is_some size then Int.toString (the size) ^ "_" else "") ^
-               extension
-           | Axiom (specialisation, extension) =>
-               Int.toString specialisation ^ "_" ^ extension
-       in
-         #prob_domain tptp_prob ^
-         Int.toString (#prob_number tptp_prob) ^
-         prob_form ^
-         suffix
-       end
-   | Nonstandard str => str
+      Standard tptp_prob =>
+        let
+          val prob_form =
+            case #prob_form tptp_prob of
+              TPTP_Syntax.THF => "_thf_"
+            | TPTP_Syntax.TFF => "_tff_"
+            | TPTP_Syntax.TFF_with_arithmetic => "_thfwa_"
+            | TPTP_Syntax.FOF => "_fof_"
+            | TPTP_Syntax.CNF => "_cnf_"
+          val suffix =
+            case #suffix tptp_prob of
+              Problem ((version, size), extension) =>
+                Int.toString version ^ "_" ^
+                (if is_some size then Int.toString (the size) ^ "_" else "") ^
+                extension
+            | Axiom (specialisation, extension) =>
+                Int.toString specialisation ^ "_" ^ extension
+        in
+          #prob_domain tptp_prob ^
+          Int.toString (#prob_number tptp_prob) ^
+          prob_form ^
+          suffix
+        end
+    | Nonstandard str => str
 
 end