--- a/src/Pure/Isar/token.ML Fri Sep 02 19:25:44 2011 +0200
+++ b/src/Pure/Isar/token.ML Fri Sep 02 20:29:39 2011 +0200
@@ -18,6 +18,7 @@
val position_of: T -> Position.T
val end_position_of: T -> Position.T
val pos_of: T -> string
+ val range: T list -> Position.range
val eof: T
val is_eof: T -> bool
val not_eof: T -> bool
@@ -122,6 +123,13 @@
val pos_of = Position.str_of o position_of;
+fun range [] = (Position.none, Position.none)
+ | range toks =
+ let
+ val start_pos = position_of (hd toks);
+ val end_pos = end_position_of (List.last toks);
+ in (start_pos, end_pos) end;
+
(* control tokens *)