author | wenzelm |
Sun, 20 Jul 2008 23:06:55 +0200 | |
changeset 27661 | a5019f9ae068 |
parent 27660 | 61fef1137a25 |
child 27662 | 34e7236443f3 |
--- a/src/Pure/General/position.ML Sun Jul 20 23:06:53 2008 +0200 +++ b/src/Pure/General/position.ML Sun Jul 20 23:06:55 2008 +0200 @@ -8,6 +8,7 @@ signature POSITION = sig type T + type range = T * T val line_of: T -> int option val column_of: T -> int option val file_of: T -> string option @@ -33,6 +34,7 @@ (* datatype position *) datatype T = Pos of (int * int) option * Markup.property list; +type range = T * T fun line_of (Pos (SOME (m, _), _)) = SOME m | line_of _ = NONE;