# HG changeset patch
# User wenzelm
# Date 898161654 -7200
# Node ID 2af6b01e7ab63f4fd4e0e6e6b78bf128b0b98eb1
# Parent  585fa380df1a4f217ea23a213e9ecd82e2850b2a
replaced warning by error_msg;

diff -r 585fa380df1a -r 2af6b01e7ab6 src/Pure/Syntax/scan.ML
--- a/src/Pure/Syntax/scan.ML	Thu Jun 18 10:52:34 1998 +0200
+++ b/src/Pure/Syntax/scan.ML	Thu Jun 18 11:20:54 1998 +0200
@@ -193,7 +193,7 @@
 
     fun drain_loop recover inp =
       drain_with (catch scanner) inp handle FAIL msg =>
-        (warning (if_none msg "Syntax error."); warning "Trying to recover ...";
+        (error_msg (if_none msg "Syntax error."); error_msg "Trying to recover ...";
           drain_loop recover (apfst snd (drain_with recover inp)));
 
     val ((ys, (state', xs')), src') =