src/Pure/General/position.ML
changeset 27661 a5019f9ae068
parent 27426 c0ef698c0904
child 27736 3703dbd0cdea
equal deleted inserted replaced
27660:61fef1137a25 27661:a5019f9ae068
     6 *)
     6 *)
     7 
     7 
     8 signature POSITION =
     8 signature POSITION =
     9 sig
     9 sig
    10   type T
    10   type T
       
    11   type range = T * T
    11   val line_of: T -> int option
    12   val line_of: T -> int option
    12   val column_of: T -> int option
    13   val column_of: T -> int option
    13   val file_of: T -> string option
    14   val file_of: T -> string option
    14   val none: T
    15   val none: T
    15   val line_file: int -> string -> T
    16   val line_file: int -> string -> T
    31 struct
    32 struct
    32 
    33 
    33 (* datatype position *)
    34 (* datatype position *)
    34 
    35 
    35 datatype T = Pos of (int * int) option * Markup.property list;
    36 datatype T = Pos of (int * int) option * Markup.property list;
       
    37 type range = T * T
    36 
    38 
    37 fun line_of (Pos (SOME (m, _), _)) = SOME m
    39 fun line_of (Pos (SOME (m, _), _)) = SOME m
    38   | line_of _ = NONE;
    40   | line_of _ = NONE;
    39 
    41 
    40 fun column_of (Pos (SOME (_, n), _)) = SOME n
    42 fun column_of (Pos (SOME (_, n), _)) = SOME n