# HG changeset patch
# User wenzelm
# Date 1621350165 -7200
# Node ID 4b1d8beed8a3c5116ba6aaff7bc2e61d1ac5b4b5
# Parent  dfc7579aae9d4617fba3a8dff03f3dc65aea6484
proper message for instances of Exn.User_Error, without extra Output.error_prefix (e.g. for Document_Build.Build_Error);

diff -r dfc7579aae9d -r 4b1d8beed8a3 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Tue May 18 16:18:39 2021 +0200
+++ b/src/Pure/General/exn.scala	Tue May 18 17:02:45 2021 +0200
@@ -119,8 +119,7 @@
   /* message */
 
   def user_message(exn: Throwable): Option[String] =
-    if (exn.getClass == classOf[RuntimeException] ||
-        exn.getClass == classOf[User_Error])
+    if (exn.isInstanceOf[User_Error] || exn.getClass == classOf[RuntimeException])
     {
       Some(proper_string(exn.getMessage) getOrElse "Error")
     }