1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 17 16:14:07 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Tue Apr 17 16:14:07 2012 +0100
     1.3 @@ -825,21 +825,16 @@
     1.4        {cautious = cautious,
     1.5         problem_name =
     1.6          SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode)
     1.7 -         file_name))
     1.8 -      }
     1.9 -    handle _(*FIXME*) =>
    1.10 -      {cautious = cautious,
    1.11 -       problem_name = NONE
    1.12 -      }
    1.13 +         file_name))}
    1.14    in interpret_file' config [] path_prefix file_name end
    1.15  
    1.16  fun import_file cautious path_prefix file_name type_map const_map thy =
    1.17    let
    1.18      val prob_name =
    1.19        TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name))
    1.20 -      handle _(*FIXME*) => TPTP_Problem_Name.Nonstandard (Path.implode file_name)
    1.21      val (result, thy') =
    1.22        interpret_file cautious path_prefix file_name type_map const_map thy
    1.23 +  (*FIXME doesn't check if problem has already been interpreted*)
    1.24    in TPTP_Data.map (cons ((prob_name, result))) thy' end
    1.25  
    1.26  val _ =

     2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML	Tue Apr 17 16:14:07 2012 +0100
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML	Tue Apr 17 16:14:07 2012 +0100
     2.3 @@ -56,7 +56,7 @@
     2.4  datatype suffix =
     2.5      Problem of
     2.6        ((*version*)int *
     2.7 -      (*size parameter*)int option) *
     2.8 +       (*size parameter*)int option) *
     2.9        (*extension*)string
    2.10    | Axiom of
    2.11        (*specialisation*)int *
    2.12 @@ -94,10 +94,10 @@
    2.13      (*NOTE there's an ambiguity in the spec: there's no way of knowing if a
    2.14      file ending in "rm" used to be "ax" or "p". Here we default to "p".*)
    2.15      val ((((prob_domain, prob_number), prob_form), suffix), rest) =
    2.16 -     Scan.finite Symbol.stopper
    2.17 -     ((alpha ^^ alpha ^^ alpha) --
    2.18 -     (numer ^^ numer ^^ numer >> to_int) --
    2.19 -     lift forms -- (prob_suffix || ax_ending)) str
    2.20 +      Scan.finite Symbol.stopper
    2.21 +      ((alpha ^^ alpha ^^ alpha) --
    2.22 +      (numer ^^ numer ^^ numer >> to_int) --
    2.23 +      lift forms -- (prob_suffix || ax_ending)) str
    2.24  
    2.25      fun parse_form str =
    2.26        case str of
    2.27 @@ -115,36 +115,41 @@
    2.28           prob_number = prob_number,
    2.29           prob_form = parse_form prob_form,
    2.30           suffix = suffix}
    2.31 -      handle _ => Nonstandard str'
    2.32      else raise TPTP_PROBLEM_NAME ("Parse error")
    2.33    end
    2.34 +  handle exn =>
    2.35 +    (*FIXME brittle*)
    2.36 +    if General.exnName exn = "FAIL" andalso General.exnMessage exn = "FAIL NONE" then
    2.37 +      (*It's very likely that the scanner failed*)
    2.38 +      Nonstandard str'
    2.39 +    else reraise exn
    2.40  
    2.41  (*Produces an ASCII encoding of a TPTP problem-file name.*)
    2.42  fun mangle_problem_name (prob : problem_name) : string =
    2.43    case prob of
    2.44 -     Standard tptp_prob =>
    2.45 -       let
    2.46 -         val prob_form =
    2.47 -           case #prob_form tptp_prob of
    2.48 -             TPTP_Syntax.THF => "_thf_"
    2.49 -           | TPTP_Syntax.TFF => "_tff_"
    2.50 -           | TPTP_Syntax.TFF_with_arithmetic => "_thfwa_"
    2.51 -           | TPTP_Syntax.FOF => "_fof_"
    2.52 -           | TPTP_Syntax.CNF => "_cnf_"
    2.53 -         val suffix =
    2.54 -           case #suffix tptp_prob of
    2.55 -             Problem ((version, size), extension) =>
    2.56 -               Int.toString version ^ "_" ^
    2.57 -               (if is_some size then Int.toString (the size) ^ "_" else "") ^
    2.58 -               extension
    2.59 -           | Axiom (specialisation, extension) =>
    2.60 -               Int.toString specialisation ^ "_" ^ extension
    2.61 -       in
    2.62 -         #prob_domain tptp_prob ^
    2.63 -         Int.toString (#prob_number tptp_prob) ^
    2.64 -         prob_form ^
    2.65 -         suffix
    2.66 -       end
    2.67 -   | Nonstandard str => str
    2.68 +      Standard tptp_prob =>
    2.69 +        let
    2.70 +          val prob_form =
    2.71 +            case #prob_form tptp_prob of
    2.72 +              TPTP_Syntax.THF => "_thf_"
    2.73 +            | TPTP_Syntax.TFF => "_tff_"
    2.74 +            | TPTP_Syntax.TFF_with_arithmetic => "_thfwa_"
    2.75 +            | TPTP_Syntax.FOF => "_fof_"
    2.76 +            | TPTP_Syntax.CNF => "_cnf_"
    2.77 +          val suffix =
    2.78 +            case #suffix tptp_prob of
    2.79 +              Problem ((version, size), extension) =>
    2.80 +                Int.toString version ^ "_" ^
    2.81 +                (if is_some size then Int.toString (the size) ^ "_" else "") ^
    2.82 +                extension
    2.83 +            | Axiom (specialisation, extension) =>
    2.84 +                Int.toString specialisation ^ "_" ^ extension
    2.85 +        in
    2.86 +          #prob_domain tptp_prob ^
    2.87 +          Int.toString (#prob_number tptp_prob) ^
    2.88 +          prob_form ^
    2.89 +          suffix
    2.90 +        end
    2.91 +    | Nonstandard str => str
    2.92  
    2.93  end