src/Pure/Isar/token.ML

--- a/src/Pure/Isar/token.ML	Tue Oct 16 17:47:23 2012 +0200
+++ b/src/Pure/Isar/token.ML	Tue Oct 16 20:23:00 2012 +0200
@@ -18,6 +18,7 @@
   val str_of_kind: kind -> string
   val position_of: T -> Position.T
   val end_position_of: T -> Position.T
+  val position_range_of: T list -> Position.range
   val pos_of: T -> string
   val eof: T
   val is_eof: T -> bool
@@ -130,6 +131,9 @@
 fun position_of (Token ((_, (pos, _)), _, _)) = pos;
 fun end_position_of (Token ((_, (_, pos)), _, _)) = pos;
 
+fun position_range_of [] = Position.no_range
+  | position_range_of toks = (position_of (hd toks), end_position_of (List.last toks));
+
 val pos_of = Position.here o position_of;