src/Pure/Syntax/lexicon.ML

 
 
 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));
 
 
 
 (** tokenize **)
 

     val scan_token =
       Scan.max (op <= o pairself snd) scan_lit scan_val >> (fn (tk, s) => Some (tk s)) ||
       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;
 
 

 
 
 (* 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)));
 
 
 (* read_var *)

     val scan =
       $$ "?" |-- $$ "'" |-- scan_vname >> tvar ||
       $$ "?" |-- 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;
 
 
 end;