# HG changeset patch
# User wenzelm
# Date 1217877859 -7200
# Node ID d3d7038fb7b575d1de5c7b18baf957b4a35b5b68
# Parent  8dbf5761a24acbedc3e01d4b5f31d1ef3018cb00
abstract type Scan.stopper, position taken from last input token;

diff -r 8dbf5761a24a -r d3d7038fb7b5 src/Pure/Isar/outer_lex.ML
--- a/src/Pure/Isar/outer_lex.ML	Mon Aug 04 21:24:17 2008 +0200
+++ b/src/Pure/Isar/outer_lex.ML	Mon Aug 04 21:24:19 2008 +0200
@@ -12,12 +12,14 @@
     String | AltString | Verbatim | Space | Comment | Malformed | Error of string | Sync | EOF
   eqtype token
   val str_of_kind: token_kind -> string
-  val stopper: token * (token -> bool)
-  val not_sync: token -> bool
-  val not_eof: token -> bool
   val range_of: token -> Position.range
   val position_of: token -> Position.T
   val pos_of: token -> string
+  val eof: token
+  val is_eof: token -> bool
+  val not_eof: token -> bool
+  val not_sync: token -> bool
+  val stopper: token Scan.stopper
   val kind_of: token -> token_kind
   val is_kind: token_kind -> token -> bool
   val keyword_with: (string -> bool) -> token -> bool
@@ -83,22 +85,7 @@
   | EOF => "end-of-file";
 
 
-(* control tokens *)
-
-val eof = Token ((Position.none, Position.none), (EOF, ""));
-
-fun is_eof (Token (_, (EOF, _))) = true
-  | is_eof _ = false;
-
-val stopper = (eof, is_eof);
-val not_eof = not o is_eof;
-
-
-fun not_sync (Token (_, (Sync, _))) = false
-  | not_sync _ = true;
-
-
-(* get position *)
+(* position *)
 
 fun range_of (Token (range, _)) = range;
 
@@ -106,6 +93,22 @@
 val pos_of = Position.str_of o position_of;
 
 
+(* control tokens *)
+
+fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
+val eof = mk_eof Position.none;
+
+fun is_eof (Token (_, (EOF, _))) = true
+  | is_eof _ = false;
+
+val not_eof = not o is_eof;
+
+fun not_sync (Token (_, (Sync, _))) = false
+  | not_sync _ = true;
+
+val stopper = Scan.stopper (fn [] => eof | toks => mk_eof (#2 (range_of (List.last toks)))) is_eof;
+
+
 (* kind of token *)
 
 fun kind_of (Token (_, (k, _))) = k;