1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Wed Apr 18 17:44:39 2012 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp.yacc	Thu Apr 19 07:25:41 2012 +0100
     1.3 @@ -197,7 +197,7 @@
     1.4  %pos int
     1.5  %eop EOF
     1.6  %noshift EOF
     1.7 -%arg (file_name) : string
     1.8 +%arg (this_file_name) : string
     1.9  
    1.10  %nonassoc LET
    1.11  %nonassoc RPAREN
    1.12 @@ -247,22 +247,22 @@
    1.13                    | cnf_annotated (( cnf_annotated ))
    1.14  
    1.15  thf_annotated : THF LPAREN name COMMA formula_role COMMA thf_formula annotations RPAREN PERIOD ((
    1.16 -  Annotated_Formula ((file_name, THFleft + 1, THFright + 1),
    1.17 +  Annotated_Formula ((this_file_name, THFleft + 1, THFright + 1),
    1.18     THF, name, formula_role, thf_formula, annotations)
    1.19  ))
    1.20  
    1.21  tff_annotated : TFF LPAREN name COMMA formula_role COMMA tff_formula annotations RPAREN PERIOD ((
    1.22 -  Annotated_Formula ((file_name, TFFleft + 1, TFFright + 1),
    1.23 +  Annotated_Formula ((this_file_name, TFFleft + 1, TFFright + 1),
    1.24     TFF, name, formula_role, tff_formula, annotations)
    1.25  ))
    1.26  
    1.27  fof_annotated : FOF LPAREN name COMMA formula_role COMMA fof_formula annotations RPAREN PERIOD ((
    1.28 -  Annotated_Formula ((file_name, FOFleft + 1, FOFright + 1),
    1.29 +  Annotated_Formula ((this_file_name, FOFleft + 1, FOFright + 1),
    1.30     FOF, name, formula_role, fof_formula, annotations)
    1.31  ))
    1.32  
    1.33  cnf_annotated : CNF LPAREN name COMMA formula_role COMMA cnf_formula annotations RPAREN PERIOD ((
    1.34 -  Annotated_Formula ((file_name, CNFleft + 1, CNFright + 1),
    1.35 +  Annotated_Formula ((this_file_name, CNFleft + 1, CNFright + 1),
    1.36     CNF, name, formula_role, cnf_formula, annotations)
    1.37  ))
    1.38  
    1.39 @@ -791,7 +791,8 @@
    1.40  useful_info : general_list (( general_list ))
    1.41  
    1.42  include_ : INCLUDE LPAREN file_name formula_selection RPAREN PERIOD ((
    1.43 -  Include (file_name, formula_selection)
    1.44 +  Include ((this_file_name, INCLUDEleft + 1, INCLUDEright + 1),
    1.45 +    file_name, formula_selection)
    1.46  ))
    1.47  
    1.48  formula_selection : COMMA LBRKT name_list RBRKT   (( name_list  ))

     2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Apr 18 17:44:39 2012 +0200
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Apr 19 07:25:41 2012 +0100
     2.3 @@ -97,6 +97,8 @@
     2.4    val interpret_file : bool -> Path.T -> Path.T -> type_map -> const_map ->
     2.5      theory -> tptp_general_meaning * theory
     2.6  
     2.7 +  type position = string * int * int
     2.8 +  exception MISINTERPRET of position list * exn
     2.9    exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula
    2.10    exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol
    2.11    exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term
    2.12 @@ -119,6 +121,8 @@
    2.13  struct
    2.14  
    2.15  open TPTP_Syntax
    2.16 +type position = string * int * int
    2.17 +exception MISINTERPRET of position list * exn
    2.18  exception MISINTERPRET_FORMULA of string * TPTP_Syntax.tptp_formula
    2.19  exception MISINTERPRET_SYMBOL of string * TPTP_Syntax.symbol
    2.20  exception MISINTERPRET_TERM of string * TPTP_Syntax.tptp_term
    2.21 @@ -672,7 +676,7 @@
    2.22  
    2.23  fun interpret_line config inc_list type_map const_map path_prefix line thy =
    2.24    case line of
    2.25 -     Include (quoted_path, inc_list) =>
    2.26 +     Include (_, quoted_path, inc_list) =>
    2.27         interpret_file'
    2.28          config
    2.29          inc_list
    2.30 @@ -685,7 +689,7 @@
    2.31          type_map
    2.32          const_map
    2.33          thy
    2.34 -   | Annotated_Formula (pos, lang, label, role, tptp_formula, annotation_opt) =>
    2.35 +   | Annotated_Formula (_, lang, label, role, tptp_formula, annotation_opt) =>
    2.36         (*interpret a line only if "label" is in "inc_list", or if "inc_list" is
    2.37            empty (in which case interpret all lines)*)
    2.38         (*FIXME could work better if inc_list were sorted*)
    2.39 @@ -779,6 +783,7 @@
    2.40               end
    2.41         else (*do nothing if we're not to includ this AF*)
    2.42           ((type_map, const_map, []), thy)
    2.43 +
    2.44  and interpret_problem config inc_list path_prefix lines type_map const_map thy =
    2.45    let
    2.46      val thy_name = Context.theory_name thy
    2.47 @@ -789,6 +794,16 @@
    2.48                 (*process the line, ignoring the type-context for variables*)
    2.49                 val ((type_map', const_map', l'), thy') =
    2.50                   interpret_line config inc_list type_map const_map path_prefix line thy
    2.51 +                   handle
    2.52 +                     (*package all exceptions to include position information,
    2.53 +                       even relating to multiple levels of "include"ed files*)
    2.54 +                       (*FIXME "exn" contents may appear garbled due to markup
    2.55 +                         FIXME this appears as ML source position *)
    2.56 +                       MISINTERPRET (pos_list, exn)  =>
    2.57 +                         raise MISINTERPRET
    2.58 +                           (TPTP_Syntax.pos_of_line line :: pos_list, exn)
    2.59 +                     | exn => raise MISINTERPRET
    2.60 +                         ([TPTP_Syntax.pos_of_line line], exn)
    2.61               in
    2.62                 ((type_map',
    2.63                   const_map',

     3.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML	Wed Apr 18 17:44:39 2012 +0200
     3.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_lexyacc.ML	Thu Apr 19 07:25:41 2012 +0100
     3.3 @@ -3717,7 +3717,7 @@
     3.4  local open Header in
     3.5  val actions = 
     3.6  fn (i392,defaultPos,stack,
     3.7 -    (file_name):arg) =>
     3.8 +    (this_file_name):arg) =>
     3.9  case (i392,stack)
    3.10  of  ( 0, ( ( _, ( MlyValue.tptp_file tptp_file, tptp_file1left, 
    3.11  tptp_file1right)) :: rest671)) => let val  result = MlyValue.tptp (
    3.12 @@ -3784,7 +3784,7 @@
    3.13  MlyValue.name name, _, _)) :: _ :: ( _, ( _, (THFleft as THF1left), 
    3.14  THFright)) :: rest671)) => let val  result = MlyValue.thf_annotated (
    3.15  (
    3.16 -  Annotated_Formula ((file_name, THFleft + 1, THFright + 1),
    3.17 +  Annotated_Formula ((this_file_name, THFleft + 1, THFright + 1),
    3.18     THF, name, formula_role, thf_formula, annotations)
    3.19  )
    3.20  )
    3.21 @@ -3797,7 +3797,7 @@
    3.22  MlyValue.name name, _, _)) :: _ :: ( _, ( _, (TFFleft as TFF1left), 
    3.23  TFFright)) :: rest671)) => let val  result = MlyValue.tff_annotated (
    3.24  (
    3.25 -  Annotated_Formula ((file_name, TFFleft + 1, TFFright + 1),
    3.26 +  Annotated_Formula ((this_file_name, TFFleft + 1, TFFright + 1),
    3.27     TFF, name, formula_role, tff_formula, annotations)
    3.28  )
    3.29  )
    3.30 @@ -3810,7 +3810,7 @@
    3.31  MlyValue.name name, _, _)) :: _ :: ( _, ( _, (FOFleft as FOF1left), 
    3.32  FOFright)) :: rest671)) => let val  result = MlyValue.fof_annotated (
    3.33  (
    3.34 -  Annotated_Formula ((file_name, FOFleft + 1, FOFright + 1),
    3.35 +  Annotated_Formula ((this_file_name, FOFleft + 1, FOFright + 1),
    3.36     FOF, name, formula_role, fof_formula, annotations)
    3.37  )
    3.38  )
    3.39 @@ -3823,7 +3823,7 @@
    3.40  MlyValue.name name, _, _)) :: _ :: ( _, ( _, (CNFleft as CNF1left), 
    3.41  CNFright)) :: rest671)) => let val  result = MlyValue.cnf_annotated (
    3.42  (
    3.43 -  Annotated_Formula ((file_name, CNFleft + 1, CNFright + 1),
    3.44 +  Annotated_Formula ((this_file_name, CNFleft + 1, CNFright + 1),
    3.45     CNF, name, formula_role, cnf_formula, annotations)
    3.46  )
    3.47  )
    3.48 @@ -5519,11 +5519,14 @@
    3.49  end
    3.50  |  ( 249, ( ( _, ( _, _, PERIOD1right)) :: _ :: ( _, ( 
    3.51  MlyValue.formula_selection formula_selection, _, _)) :: ( _, ( 
    3.52 -MlyValue.file_name file_name, _, _)) :: _ :: ( _, ( _, INCLUDE1left, _
    3.53 -)) :: rest671)) => let val  result = MlyValue.include_ (
    3.54 +MlyValue.file_name file_name, _, _)) :: _ :: ( _, ( _, (INCLUDEleft
    3.55 + as INCLUDE1left), INCLUDEright)) :: rest671)) => let val  result = 
    3.56 +MlyValue.include_ (
    3.57  (
    3.58 -  Include (file_name, formula_selection)
    3.59 -))
    3.60 +  Include ((this_file_name, INCLUDEleft + 1, INCLUDEright + 1),
    3.61 +    file_name, formula_selection)
    3.62 +)
    3.63 +)
    3.64   in ( LrTable.NT 132, ( result, INCLUDE1left, PERIOD1right), rest671)
    3.65  
    3.66  end

     4.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Wed Apr 18 17:44:39 2012 +0200
     4.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Thu Apr 19 07:25:41 2012 +0100
     4.3 @@ -131,7 +131,7 @@
     4.4    datatype tptp_line =
     4.5        Annotated_Formula of position * language * string * role *
     4.6          tptp_formula * annotation option
     4.7 -   |  Include of string * string list
     4.8 +   |  Include of position * string * string list
     4.9  
    4.10    type tptp_problem = tptp_line list
    4.11  
    4.12 @@ -143,6 +143,8 @@
    4.13  
    4.14    val nameof_tff_atom_type : tptp_type -> string
    4.15  
    4.16 +  val pos_of_line : tptp_line -> position
    4.17 +
    4.18    (*Returns the list of all files included in a directory and its
    4.19    subdirectories. This is only used for testing the parser/interpreter against
    4.20    all THF problems.*)
    4.21 @@ -275,7 +277,7 @@
    4.22  
    4.23  datatype tptp_line =
    4.24      Annotated_Formula of position * language * string * role * tptp_formula * annotation option
    4.25 - |  Include of string * string list
    4.26 + |  Include of position * string * string list
    4.27  
    4.28  type tptp_problem = tptp_line list
    4.29  
    4.30 @@ -284,6 +286,11 @@
    4.31  fun nameof_tff_atom_type (Atom_type str) = str
    4.32    | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
    4.33  
    4.34 +fun pos_of_line tptp_line =
    4.35 +  case tptp_line of
    4.36 +      Annotated_Formula (position, _, _, _, _, _) => position
    4.37 +   |  Include (position, _, _) => position
    4.38 +
    4.39  (*Used for debugging. Returns all files contained within a directory or its
    4.40  subdirectories. Follows symbolic links, filters away directories.*)
    4.41  fun get_file_list path =