# HG changeset patch
# User wenzelm
# Date 1217883310 -7200
# Node ID 302e9c8c489b9b25480f6dc8987d78d4f083a3be
# Parent  3703dbd0cdea5404574d9572fc203b9d83250757
position scanner: encode token range;

diff -r 3703dbd0cdea -r 302e9c8c489b src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Mon Aug 04 22:55:08 2008 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Mon Aug 04 22:55:10 2008 +0200
@@ -136,7 +136,8 @@
 
 val not_eof = Scan.one T.not_eof;
 
-fun position scan = (Scan.ahead not_eof >> T.position_of) -- scan >> Library.swap;
+fun position scan =
+  (Scan.ahead not_eof >> (Position.encode_range o T.range_of)) -- scan >> Library.swap;
 
 fun kind k =
   group (T.str_of_kind k) (Scan.one (T.is_kind k) >> T.val_of);