src/Pure/General/position.ML
changeset 31424 d30a867a86fb
parent 30669 6de7ef888aa3
child 31435 d24ef3ff34bc
equal deleted inserted replaced
31423:79e707bb0d6b 31424:d30a867a86fb
     5 *)
     5 *)
     6 
     6 
     7 signature POSITION =
     7 signature POSITION =
     8 sig
     8 sig
     9   type T
     9   type T
       
    10   val value: string -> int -> Properties.T
    10   val line_of: T -> int option
    11   val line_of: T -> int option
    11   val column_of: T -> int option
    12   val column_of: T -> int option
    12   val offset_of: T -> int option
    13   val offset_of: T -> int option
    13   val file_of: T -> string option
    14   val file_of: T -> string option
    14   val advance: Symbol.symbol -> T -> T
    15   val advance: Symbol.symbol -> T -> T