src/Pure/Syntax/scan.ML
changeset 5987 389d03e6e093
parent 5869 b279a84ac11c
equal deleted inserted replaced
5986:6ebbc9e7cc20 5987:389d03e6e093
   206   let
   206   let
   207     fun drain_with scan = drain def_prmpt get stopper scan;
   207     fun drain_with scan = drain def_prmpt get stopper scan;
   208 
   208 
   209     fun drain_loop recover inp =
   209     fun drain_loop recover inp =
   210       drain_with (catch scanner) inp handle FAIL msg =>
   210       drain_with (catch scanner) inp handle FAIL msg =>
   211         (error_msg (if_none msg "Syntax error."); error_msg "Trying to recover ...";
   211         (error_msg (if_none msg "Syntax error.");
   212           drain_loop recover (apfst snd (drain_with recover inp)));
   212           drain_loop recover (apfst snd (drain_with recover inp)));
   213 
   213 
   214     val ((ys, (state', xs')), src') =
   214     val ((ys, (state', xs')), src') =
   215       (case (get def_prmpt src, opt_recover) of
   215       (case (get def_prmpt src, opt_recover) of
   216         (([], s), _) => (([], (state, [])), s)
   216         (([], s), _) => (([], (state, [])), s)