src/Pure/General/position.ML
changeset 31439 d24ef3ff34bc
parent 31428 d30a867a86fb
child 32195 d77476e4040c
equal deleted inserted replaced
31438:1f9b6a5dc8cc 31439:d24ef3ff34bc
    14   val file_of: T -> string option
    14   val file_of: T -> string option
    15   val advance: Symbol.symbol -> T -> T
    15   val advance: Symbol.symbol -> T -> T
    16   val distance_of: T -> T -> int
    16   val distance_of: T -> T -> int
    17   val none: T
    17   val none: T
    18   val start: T
    18   val start: T
       
    19   val file_name: string -> Properties.T
    19   val file: string -> T
    20   val file: string -> T
    20   val line: int -> T
    21   val line: int -> T
    21   val line_file: int -> string -> T
    22   val line_file: int -> string -> T
    22   val id: string -> T
    23   val id: string -> T
    23   val get_id: T -> string option
    24   val get_id: T -> string option