# HG changeset patch
# User wenzelm
# Date 1216588015 -7200
# Node ID a5019f9ae06812fa0a51e4f952d7f68f81847362
# Parent  61fef1137a25f66ace8bc6a2c0981dd8039fbdea
added type range;

diff -r 61fef1137a25 -r a5019f9ae068 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;