# HG changeset patch
# User wenzelm
# Date 1489659909 -3600
# Node ID 50f956a1ac3f8996cd39eb9806e685040dc91223
# Parent  7611c55c39d06b28d8097293d672879499664d55
clarified message: exception output usally happens in a context without extra newline;

diff -r 7611c55c39d0 -r 50f956a1ac3f src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Wed Mar 15 21:52:04 2017 +0100
+++ b/src/Pure/General/exn.scala	Thu Mar 16 11:25:09 2017 +0100
@@ -20,7 +20,7 @@
       }
     override def hashCode: Int = message.hashCode
 
-    override def toString: String = Output.error_text(message)
+    override def toString: String = "\n" + Output.error_text(message)
   }
 
   object ERROR
diff -r 7611c55c39d0 -r 50f956a1ac3f src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 21:52:04 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Mar 16 11:25:09 2017 +0100
@@ -415,7 +415,7 @@
 
     // adhoc patch of confusing message
     val orig_plugin_error = jEdit.getProperty("plugin-error.start-error")
-    jEdit.setProperty("plugin-error.start-error", "Cannot start plugin:\n{0}")
+    jEdit.setProperty("plugin-error.start-error", "Cannot start plugin: {0}")
 
     init_options()
     init_resources()