changeset 27661 | a5019f9ae068 |
parent 27426 | c0ef698c0904 |
child 27736 | 3703dbd0cdea |
--- 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;