src/Pure/Syntax/scan.ML
changeset 5048 2af6b01e7ab6
parent 4968 c68a9c510c90
child 5861 7536314d9a5f
equal deleted inserted replaced
5047:585fa380df1a 5048:2af6b01e7ab6
   191   let
   191   let
   192     fun drain_with scan = drain def_prmpt get stopper scan;
   192     fun drain_with scan = drain def_prmpt get stopper scan;
   193 
   193 
   194     fun drain_loop recover inp =
   194     fun drain_loop recover inp =
   195       drain_with (catch scanner) inp handle FAIL msg =>
   195       drain_with (catch scanner) inp handle FAIL msg =>
   196         (warning (if_none msg "Syntax error."); warning "Trying to recover ...";
   196         (error_msg (if_none msg "Syntax error."); error_msg "Trying to recover ...";
   197           drain_loop recover (apfst snd (drain_with recover inp)));
   197           drain_loop recover (apfst snd (drain_with recover inp)));
   198 
   198 
   199     val ((ys, (state', xs')), src') =
   199     val ((ys, (state', xs')), src') =
   200       (case (get def_prmpt src, opt_recover) of
   200       (case (get def_prmpt src, opt_recover) of
   201         (([], s), _) => (([], (state, [])), s)
   201         (([], s), _) => (([], (state, [])), s)