# HG changeset patch
# User wenzelm
# Date 1406830170 -7200
# Node ID 885888a880fb9789ff1318025bf464c7658e9be5
# Parent  2d0f0d6fdf3ea2f6be2394530e03704531b6ca2c
more general notion of "user error" including empty message -- NB: Output.error_message needs non-empty string to emit anything;

diff -r 2d0f0d6fdf3e -r 885888a880fb src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Wed Jul 30 09:40:28 2014 +0200
+++ b/src/Pure/General/exn.scala	Thu Jul 31 20:09:30 2014 +0200
@@ -82,7 +82,7 @@
     }
     else if (exn.getClass == runtime_exception) {
       val msg = exn.getMessage
-      Some(if (msg == null) "Error" else msg)
+      Some(if (msg == null || msg == "") "Error" else msg)
     }
     else if (exn.isInstanceOf[RuntimeException]) Some(exn.toString)
     else None
diff -r 2d0f0d6fdf3e -r 885888a880fb src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Wed Jul 30 09:40:28 2014 +0200
+++ b/src/Pure/Isar/runtime.ML	Thu Jul 31 20:09:30 2014 +0200
@@ -99,6 +99,7 @@
               TERMINATE => "Exit"
             | TimeLimit.TimeOut => "Timeout"
             | TOPLEVEL_ERROR => "Error"
+            | ERROR "" => "Error"
             | ERROR msg => msg
             | Fail msg => raised exn "Fail" [msg]
             | THEORY (msg, thys) =>
diff -r 2d0f0d6fdf3e -r 885888a880fb src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Jul 30 09:40:28 2014 +0200
+++ b/src/Pure/library.ML	Thu Jul 31 20:09:30 2014 +0200
@@ -266,6 +266,7 @@
 fun error msg = raise ERROR msg;
 
 fun cat_error "" msg = error msg
+  | cat_error msg "" = error msg
   | cat_error msg1 msg2 = error (msg1 ^ "\n" ^ msg2);
 
 fun assert_all pred list msg =
diff -r 2d0f0d6fdf3e -r 885888a880fb src/Pure/library.scala
--- a/src/Pure/library.scala	Wed Jul 30 09:40:28 2014 +0200
+++ b/src/Pure/library.scala	Thu Jul 31 20:09:30 2014 +0200
@@ -25,6 +25,7 @@
 
   def cat_message(msg1: String, msg2: String): String =
     if (msg1 == "") msg2
+    else if (msg2 == "") msg1
     else msg1 + "\n" + msg2
 
   def cat_error(msg1: String, msg2: String): Nothing =