abstract type Scan.stopper;

--- a/src/Pure/General/source.ML	Mon Aug 04 21:24:15 2008 +0200
+++ b/src/Pure/General/source.ML	Mon Aug 04 21:24:17 2008 +0200
@@ -21,10 +21,10 @@
   val of_string: string -> (string, string list) source
   val exhausted: ('a, 'b) source -> ('a, 'a list) source
   val tty: (string, unit) source
-  val source': 'a -> 'b * ('b -> bool) -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
+  val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) ->
     (bool * (string -> 'a * 'b list -> 'c list * ('a * 'b list))) option ->
     ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source
-  val source: 'a * ('a -> bool) -> ('a list -> 'b list * 'a list) ->
+  val source: 'a Scan.stopper -> ('a list -> 'b list * 'a list) ->
     (bool * (string -> 'a list -> 'b list * 'a list)) option ->
     ('a, 'd) source -> ('b, ('a, 'd) source) source
 end;
@@ -148,7 +148,7 @@
         | SOME (interactive, recover) =>
             (drain (Scan.catch scan) inp handle Fail msg =>
               (if interactive then Output.error_msg msg else ();
-                drain (Scan.unless (Scan.lift (Scan.one (#2 stopper))) (recover msg)) inp)));
+                drain (Scan.unless (Scan.lift (Scan.one (Scan.is_stopper stopper))) (recover msg)) inp)));
   in (ys, (state', unget (xs', src'))) end;
 
 fun source' init_state stopper scan recover src =

--- a/src/Pure/General/symbol.ML	Mon Aug 04 21:24:15 2008 +0200
+++ b/src/Pure/General/symbol.ML	Mon Aug 04 21:24:17 2008 +0200
@@ -21,7 +21,7 @@
   val is_utf8_trailer: symbol -> bool
   val eof: symbol
   val is_eof: symbol -> bool
-  val stopper: symbol * (symbol -> bool)
+  val stopper: symbol Scan.stopper
   val sync: symbol
   val is_sync: symbol -> bool
   val malformed: symbol
@@ -120,7 +120,7 @@
 val eof = "";
 fun is_eof s = s = eof;
 fun not_eof s = s <> eof;
-val stopper = (eof, is_eof);
+val stopper = Scan.stopper (K eof) is_eof;
 
 val sync = "\\<^sync>";
 fun is_sync s = s = sync;

--- a/src/Pure/Isar/args.ML	Mon Aug 04 21:24:15 2008 +0200
+++ b/src/Pure/Isar/args.ML	Mon Aug 04 21:24:17 2008 +0200
@@ -23,7 +23,7 @@
   val mk_fact: thm list -> T
   val mk_attribute: (morphism -> attribute) -> T
   val eof: T
-  val stopper: T * (T -> bool)
+  val stopper: T Scan.stopper
   val not_eof: T -> bool
   type src
   val src: (string * T list) * Position.T -> src
@@ -161,7 +161,7 @@
 fun is_eof (Arg ((EOF, _, _), _)) = true
   | is_eof _ = false;
 
-val stopper = (eof, is_eof);
+val stopper = Scan.stopper (K eof) is_eof;
 val not_eof = not o is_eof;
 
 

--- a/src/Pure/ML/ml_lex.ML	Mon Aug 04 21:24:15 2008 +0200
+++ b/src/Pure/ML/ml_lex.ML	Mon Aug 04 21:24:17 2008 +0200
@@ -11,7 +11,7 @@
     Keyword | Ident | LongIdent | TypeVar | Word | Int | Real | Char | String |
     Space | Comment | Error of string | EOF
   eqtype token
-  val stopper: token * (token -> bool)
+  val stopper: token Scan.stopper
   val is_regular: token -> bool
   val is_improper: token -> bool
   val pos_of: token -> string
@@ -43,7 +43,7 @@
 fun is_eof (Token (_, (EOF, _))) = true
   | is_eof _ = false;
 
-val stopper = (eof, is_eof);
+val stopper = Scan.stopper (K eof) is_eof;
 
 
 fun is_regular (Token (_, (Error _, _))) = false

--- a/src/Pure/Syntax/simple_syntax.ML	Mon Aug 04 21:24:15 2008 +0200
+++ b/src/Pure/Syntax/simple_syntax.ML	Mon Aug 04 21:24:17 2008 +0200
@@ -22,7 +22,7 @@
 val eof = Lexicon.EndToken;
 fun is_eof tk = tk = Lexicon.EndToken;
 
-val stopper = (eof, is_eof);
+val stopper = Scan.stopper (K eof) is_eof;
 val not_eof = not o is_eof;
 
 val lexicon = Scan.make_lexicon

--- a/src/Pure/Thy/thy_output.ML	Mon Aug 04 21:24:15 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon Aug 04 21:24:17 2008 +0200
@@ -363,12 +363,11 @@
 
     (* spans *)
 
-    val stopper =
-      ((NONE, (BasicToken (#1 T.stopper), ("", 0))),
-        fn (_, (BasicToken x, _)) => #2 T.stopper x | _ => false);
+    val is_eof = fn (_, (BasicToken x, _)) => T.is_eof x | _ => false;
+    val stopper = Scan.stopper (K (NONE, (BasicToken T.eof, ("", 0)))) is_eof;
 
     val cmd = Scan.one (is_some o fst);
-    val non_cmd = Scan.one (is_none o fst andf not o #2 stopper) >> #2;
+    val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2;
 
     val comments = Scan.many (comment_token o fst o snd);
     val blank = Scan.one (blank_token o fst o snd);