clarified message: exception output usally happens in a context without extra newline;
--- 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
--- 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()