proper message for instances of Exn.User_Error, without extra Output.error_prefix (e.g. for Document_Build.Build_Error);

--- 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")
     }