1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML	Tue Apr 17 23:22:40 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_problem_name.ML	Tue Apr 17 23:22:40 2012 +0100
     1.3 @@ -87,17 +87,17 @@
     1.4  
     1.5  exception TPTP_PROBLEM_NAME of string
     1.6  
     1.7 -(*FIXME add graceful handling on non-wellformed TPTP filenames*)
     1.8  fun parse_problem_name str' : problem_name =
     1.9    let
    1.10      val str = Symbol.explode str'
    1.11      (*NOTE there's an ambiguity in the spec: there's no way of knowing if a
    1.12      file ending in "rm" used to be "ax" or "p". Here we default to "p".*)
    1.13 -    val ((((prob_domain, prob_number), prob_form), suffix), rest) =
    1.14 +    val (parsed_name, rest) =
    1.15        Scan.finite Symbol.stopper
    1.16 -      ((alpha ^^ alpha ^^ alpha) --
    1.17 -      (numer ^^ numer ^^ numer >> to_int) --
    1.18 -      lift forms -- (prob_suffix || ax_ending)) str
    1.19 +      (((alpha ^^ alpha ^^ alpha) --
    1.20 +       (numer ^^ numer ^^ numer >> to_int) --
    1.21 +       lift forms -- (prob_suffix || ax_ending)) >> SOME
    1.22 +      || Scan.succeed NONE) str
    1.23  
    1.24      fun parse_form str =
    1.25        case str of
    1.26 @@ -108,21 +108,19 @@
    1.27        | "-" => TPTP_Syntax.CNF
    1.28        | _ => raise TPTP_PROBLEM_NAME ("Unknown TPTP form: " ^ str)
    1.29    in
    1.30 -    if null rest (*check if the whole name was parsed*)
    1.31 -    then
    1.32 -      Standard
    1.33 -        {prob_domain = prob_domain,
    1.34 -         prob_number = prob_number,
    1.35 -         prob_form = parse_form prob_form,
    1.36 -         suffix = suffix}
    1.37 -    else raise TPTP_PROBLEM_NAME ("Parse error")
    1.38 +    if not (null rest) orelse is_none parsed_name then Nonstandard str'
    1.39 +    else
    1.40 +      let
    1.41 +        val (((prob_domain, prob_number), prob_form), suffix) =
    1.42 +          the parsed_name
    1.43 +      in
    1.44 +        Standard
    1.45 +          {prob_domain = prob_domain,
    1.46 +           prob_number = prob_number,
    1.47 +           prob_form = parse_form prob_form,
    1.48 +           suffix = suffix}
    1.49 +      end
    1.50    end
    1.51 -  handle exn =>
    1.52 -    (*FIXME brittle*)
    1.53 -    if General.exnName exn = "FAIL" andalso General.exnMessage exn = "FAIL NONE" then
    1.54 -      (*It's very likely that the scanner failed*)
    1.55 -      Nonstandard str'
    1.56 -    else reraise exn
    1.57  
    1.58  (*Produces an ASCII encoding of a TPTP problem-file name.*)
    1.59  fun mangle_problem_name (prob : problem_name) : string =