# HG changeset patch
# User wenzelm
# Date 1489519064 -3600
# Node ID f3ba27dfaecacdff398ed61dfcb35edb61d30001
# Parent  4fa82bbb394e28fbe24d2edc01091b9c3ce8a0bf
show user error as on command-line, e.g. relevant for unexpected crashes;

diff -r 4fa82bbb394e -r f3ba27dfaeca src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Tue Mar 14 19:46:53 2017 +0100
+++ b/src/Pure/General/exn.scala	Tue Mar 14 20:17:44 2017 +0100
@@ -20,7 +20,7 @@
       }
     override def hashCode: Int = message.hashCode
 
-    override def toString: String = "ERROR(" + Output.clean_yxml(message) + ")"
+    override def toString: String = Output.error_text(message)
   }
 
   object ERROR