src/Pure/General/symbol.ML
changeset 8998 56c44eee46ad
parent 8806 a202293db3f6
child 9961 5a9626118941
equal deleted inserted replaced
8997:da290d99d8b2 8998:56c44eee46ad
   245     None => c
   245     None => c
   246   | Some s => "\\" ^ s);
   246   | Some s => "\\" ^ s);
   247 
   247 
   248 
   248 
   249 
   249 
   250 (** scanning though symbols **)
   250 (** scanning through symbols **)
   251 
   251 
   252 fun scanner msg scan chs =
   252 fun scanner msg scan chs =
   253   let
   253   let
   254     fun err_msg cs = msg ^ ": " ^ beginning cs;
   254     fun err_msg cs = msg ^ ": " ^ beginning cs;
   255     val fin_scan = Scan.error (Scan.finite stopper (!! (fn (cs, _) => err_msg cs) scan));
   255     val fin_scan = Scan.error (Scan.finite stopper (!! (fn (cs, _) => err_msg cs) scan));