added type range;
authorwenzelm
Sun, 20 Jul 2008 23:06:55 +0200
changeset 27661 a5019f9ae068
parent 27660 61fef1137a25
child 27662 34e7236443f3
added type range;
src/Pure/General/position.ML
--- 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;