# HG changeset patch
# User wenzelm
# Date 1407001112 -7200
# Node ID ae3eac418c5f1d5139e5be1c3732d57665b7ca88
# Parent  d8966c09025c20674baa4b07cb78bcc54ab0d664
more emphatic warning via error_message (violating historic TTY protocol);

diff -r d8966c09025c -r ae3eac418c5f src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat Aug 02 19:29:02 2014 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Aug 02 19:38:32 2014 +0200
@@ -204,7 +204,7 @@
   in
     (case res of
       NONE => st0
-    | SOME st => (warning (Toplevel.type_error tr st0 ^ " -- resetting state"); st))
+    | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st))
   end) ();
 
 fun run int tr st =