Symbol.stopper;

--- a/src/Pure/Syntax/lexicon.ML	Mon May 18 17:57:16 1998 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Mon May 18 17:57:47 1998 +0200
@@ -236,7 +236,7 @@
 fun implode_xstr cs = enclose "''" "''" (implode (map (fn "'" => "\\'" | c => c) cs));
 
 fun explode_xstr str =
-  #1 (Scan.error (Scan.finite Symbol.eof scan_str) (Symbol.explode str));
+  #1 (Scan.error (Scan.finite Symbol.stopper scan_str) (Symbol.explode str));
 
 
 
@@ -263,7 +263,7 @@
       scan_str >> (Some o StrSy o implode_xstr) ||
       Scan.one Symbol.is_blank >> K None;
   in
-    (case Scan.error (Scan.finite Symbol.eof (Scan.repeat scan_token)) chs of
+    (case Scan.error (Scan.finite Symbol.stopper (Scan.repeat scan_token)) chs of
       (toks, []) => mapfilter I toks @ [EndToken]
     | (_, cs) => error ("Inner lexical error at: " ^ quote (implode cs)))
   end;
@@ -297,7 +297,7 @@
 (* indexname *)
 
 fun indexname cs =
-  (case Scan.error (Scan.finite Symbol.eof (Scan.option scan_vname)) cs of
+  (case Scan.error (Scan.finite Symbol.stopper (Scan.option scan_vname)) cs of
     (Some xi, []) => xi
   | _ => error ("Lexical error in variable name: " ^ quote (implode cs)));
 
@@ -317,7 +317,7 @@
       $$ "?" |-- scan_vname >> var ||
       Scan.any Symbol.not_eof >> (free o implode);
   in
-    #1 (Scan.error (Scan.finite Symbol.eof scan) (Symbol.explode str))
+    #1 (Scan.error (Scan.finite Symbol.stopper scan) (Symbol.explode str))
   end;
 
 

--- a/src/Pure/Syntax/symbol.ML	Mon May 18 17:57:16 1998 +0200
+++ b/src/Pure/Syntax/symbol.ML	Mon May 18 17:57:47 1998 +0200
@@ -12,6 +12,7 @@
   val eof: symbol
   val is_eof: symbol -> bool
   val not_eof: symbol -> bool
+  val stopper: symbol * (symbol -> bool)
   val is_ascii: symbol -> bool
   val is_letter: symbol -> bool
   val is_digit: symbol -> bool
@@ -170,6 +171,7 @@
 
 fun is_eof s = s = eof;
 fun not_eof s = s <> eof;
+val stopper = (eof, is_eof);
 
 fun is_ascii s = size s = 1 andalso ord s < 128;
 
@@ -217,7 +219,7 @@
 fun sym_explode str =
   let val chs = explode str in
     if no_syms chs then chs     (*tune trivial case*)
-    else map symbol (#1 (Scan.error (Scan.finite eof (Scan.repeat scan)) chs))
+    else map symbol (#1 (Scan.error (Scan.finite stopper (Scan.repeat scan)) chs))
   end;
 
 

--- a/src/Pure/Syntax/syn_ext.ML	Mon May 18 17:57:16 1998 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Mon May 18 17:57:47 1998 +0200
@@ -189,7 +189,7 @@
     $$ "'" -- Scan.one Symbol.is_blank >> K None;
 
   val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
-  val read_symbs = mapfilter I o #1 o Scan.error (Scan.finite Symbol.eof scan_symbs);
+  val read_symbs = mapfilter I o #1 o Scan.error (Scan.finite Symbol.stopper scan_symbs);
 in
   val read_mixfix = read_symbs o Symbol.explode;
 end;

--- a/src/Pure/Thy/thy_scan.ML	Mon May 18 17:57:16 1998 +0200
+++ b/src/Pure/Thy/thy_scan.ML	Mon May 18 17:57:47 1998 +0200
@@ -144,7 +144,7 @@
     val scan_toks = Scan.repeat (scan_token lex);
     val ignore = fn (Ignore, _, _) => true | _ => false;
   in
-    (case Scan.error (Scan.finite' Symbol.eof scan_toks) (Some 1, chs) of
+    (case Scan.error (Scan.finite' Symbol.stopper scan_toks) (Some 1, chs) of
       (toks, (n, [])) => filter_out ignore toks @ [token EOF n "end-of-file"]
     | (_, (n, cs)) => error (lex_err n ("Bad input " ^ quote (beginning cs))))
   end;

--- a/src/Pure/section_utils.ML	Mon May 18 17:57:16 1998 +0200
+++ b/src/Pure/section_utils.ML	Mon May 18 17:57:47 1998 +0200
@@ -34,7 +34,7 @@
 (*Skipping initial blanks, find the first identifier*)	(* FIXME *)
 fun scan_to_id s = 
     s |> Symbol.explode
-    |> Scan.error (Scan.finite Symbol.eof
+    |> Scan.error (Scan.finite Symbol.stopper
       (!! (fn _ => "Expected to find an identifier in " ^ s)
         (Scan.any Symbol.is_blank |-- Syntax.scan_id)))
     |> #1;