# HG changeset patch
# User wenzelm
# Date 1398252512 -7200
# Node ID 06853449cf0a94fc598c6bea8a3494efaf251508
# Parent  3f23441453d0b2232bcac7e6d20671918f71db95
explicit Exn.error_message in accordance to Output.error_message in ML;

diff -r 3f23441453d0 -r 06853449cf0a src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Wed Apr 23 13:05:11 2014 +0200
+++ b/src/Pure/General/exn.scala	Wed Apr 23 13:28:32 2014 +0200
@@ -73,5 +73,11 @@
 
   def message(exn: Throwable): String =
     user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
+
+
+  /* TTY error message */
+
+  def error_message(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
+  def error_message(exn: Throwable): String = error_message(message(exn))
 }
 
diff -r 3f23441453d0 -r 06853449cf0a src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Apr 23 13:05:11 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Apr 23 13:28:32 2014 +0200
@@ -88,8 +88,8 @@
         }
         catch {
           case exn: Throwable =>
-            System.err.println("Failed to initialize protocol handler: " +
-              name + "\n" + Exn.message(exn))
+            System.err.println(Exn.error_message(
+              "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn)))
             (handlers1, functions1)
         }
 
@@ -102,8 +102,8 @@
           try { functions(a)(msg) }
           catch {
             case exn: Throwable =>
-              System.err.println("Failed invocation of protocol function: " +
-                quote(a) + "\n" + Exn.message(exn))
+              System.err.println(Exn.error_message(
+                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn)))
             false
           }
         case _ => false
diff -r 3f23441453d0 -r 06853449cf0a src/Pure/System/command_line.scala
--- a/src/Pure/System/command_line.scala	Wed Apr 23 13:05:11 2014 +0200
+++ b/src/Pure/System/command_line.scala	Wed Apr 23 13:28:32 2014 +0200
@@ -30,7 +30,7 @@
       catch {
         case exn: Throwable =>
           if (debug) exn.printStackTrace
-          System.err.println(cat_lines(split_lines(Exn.message(exn)).map("*** " + _)))
+          System.err.println(Exn.error_message(exn))
           Exn.return_code(exn, 2)
       }
     sys.exit(rc)
diff -r 3f23441453d0 -r 06853449cf0a src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Wed Apr 23 13:05:11 2014 +0200
+++ b/src/Pure/Tools/main.scala	Wed Apr 23 13:28:32 2014 +0200
@@ -60,7 +60,9 @@
                     build_heap = true, more_dirs = more_dirs,
                     system_mode = system_mode, sessions = List(session)))
               }
-              catch { case exn: Throwable => (Exn.message(exn) + "\n", Exn.return_code(exn, 2)) }
+              catch {
+                case exn: Throwable => (Exn.error_message(exn) + "\n", Exn.return_code(exn, 2))
+              }
 
             system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
             system_dialog.return_code(rc)
diff -r 3f23441453d0 -r 06853449cf0a src/Tools/Graphview/src/graphview.scala
--- a/src/Tools/Graphview/src/graphview.scala	Wed Apr 23 13:05:11 2014 +0200
+++ b/src/Tools/Graphview/src/graphview.scala	Wed Apr 23 13:28:32 2014 +0200
@@ -34,7 +34,7 @@
           case _ => error("Bad arguments:\n" + cat_lines(args))
         }
       }
-      catch { case exn: Throwable => println(Exn.message(exn)); sys.exit(1) }
+      catch { case exn: Throwable => println(Exn.error_message(exn)); sys.exit(1) }
 
     val top = new MainFrame {
       iconImage = GUI.isabelle_image()