# HG changeset patch
# User wenzelm
# Date 1398771133 -7200
# Node ID 433cf57550fa4d653a0b164fd3368ae6673f7f53
# Parent  f2eb0f22589f7c37601284568f08eea831a4f994
more systematic Isabelle output, like in classic Isabelle/ML (without markup);

diff -r f2eb0f22589f -r 433cf57550fa src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/Concurrent/consumer_thread.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -36,7 +36,7 @@
   def is_active: Boolean = active && thread.isAlive
 
   private def failure(exn: Throwable): Unit =
-    System.err.println(
+    Output.error_message(
       "Consumer thread failure: " + quote(thread.getName) + "\n" + Exn.message(exn))
 
   private def robust_finish(): Unit =
diff -r f2eb0f22589f -r 433cf57550fa src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/General/completion.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -62,7 +62,7 @@
     def load(): History =
     {
       def ignore_error(msg: String): Unit =
-        System.err.println("### Ignoring bad content of file " + COMPLETION_HISTORY +
+        Output.warning("Ignoring bad content of file " + COMPLETION_HISTORY +
           (if (msg == "") "" else "\n" + msg))
 
       val content =
diff -r f2eb0f22589f -r 433cf57550fa src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/General/exn.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -73,11 +73,5 @@
 
   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 f2eb0f22589f -r 433cf57550fa src/Pure/General/output.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/output.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -0,0 +1,18 @@
+/*  Title:      Pure/General/output.ML
+    Author:     Makarius
+
+Isabelle output channels: plain text without markup.
+*/
+
+package isabelle
+
+
+object Output
+{
+  def warning_text(msg: String): String = cat_lines(split_lines(msg).map("### " + _))
+  def error_text(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
+
+  def warning(msg: String) { System.err.println(warning_text(msg)) }
+  def error_message(msg: String) { System.err.println(error_text(msg)) }
+}
+
diff -r f2eb0f22589f -r 433cf57550fa src/Pure/General/timing.scala
--- a/src/Pure/General/timing.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/General/timing.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -20,7 +20,7 @@
 
       val timing = stop - start
       if (timing.is_relevant)
-        System.err.println(
+        Output.warning(
           (if (message == null || message.isEmpty) "" else message + ": ") +
             timing.message + " elapsed time")
 
diff -r f2eb0f22589f -r 433cf57550fa src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -179,14 +179,14 @@
                   add_status(markup).
                   add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem))
               case _ =>
-                System.err.println("Ignored status message: " + msg)
+                Output.warning("Ignored status message: " + msg)
                 state
             })
 
         case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
           (this /: msgs)((state, msg) =>
             {
-              def bad(): Unit = System.err.println("Ignored report message: " + msg)
+              def bad(): Unit = Output.warning("Ignored report message: " + msg)
 
               msg match {
                 case XML.Elem(
@@ -238,7 +238,7 @@
               st
 
             case _ =>
-              System.err.println("Ignored message without serial number: " + message)
+              Output.warning("Ignored message without serial number: " + message)
               this
           }
     }
diff -r f2eb0f22589f -r 433cf57550fa src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -153,7 +153,7 @@
           if (body.forall(e => new_range.contains(e._1)))
             new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
           else {
-            System.err.println("Ignored overlapping markup information: " + new_markup +
+            Output.warning("Ignored overlapping markup information: " + new_markup +
               body.filter(e => !new_range.contains(e._1)).mkString("\n"))
             this
           }
diff -r f2eb0f22589f -r 433cf57550fa src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -37,7 +37,7 @@
           try { c.consume(a) }
           catch {
             case exn: Throwable =>
-              System.err.println("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
+              Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
           })
       }
     }
@@ -115,7 +115,7 @@
       val (handlers1, functions1) =
         handlers.get(name) match {
           case Some(old_handler) =>
-            System.err.println("Redefining protocol handler: " + name)
+            Output.warning("Redefining protocol handler: " + name)
             old_handler.stop(prover)
             (handlers - name, functions -- old_handler.functions.keys)
           case None => (handlers, functions)
@@ -135,8 +135,8 @@
         }
         catch {
           case exn: Throwable =>
-            System.err.println(Exn.error_message(
-              "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn)))
+            Output.error_message(
+              "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
             (handlers1, functions1)
         }
 
@@ -149,8 +149,8 @@
           try { functions(a)(msg) }
           catch {
             case exn: Throwable =>
-              System.err.println(Exn.error_message(
-                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn)))
+              Output.error_message(
+                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
             false
           }
         case _ => false
@@ -381,7 +381,7 @@
               global_state.change(_.define_blob(digest))
               prover.get.define_blob(digest, blob.bytes)
             case None =>
-              System.err.println("Missing blob for SHA1 digest " + digest)
+              Output.error_message("Missing blob for SHA1 digest " + digest)
           }
         }
 
@@ -411,7 +411,7 @@
       def bad_output()
       {
         if (verbose)
-          System.err.println("Ignoring bad prover output: " + output.message.toString)
+          Output.warning("Ignoring bad prover output: " + output.message.toString)
       }
 
       def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
diff -r f2eb0f22589f -r 433cf57550fa src/Pure/System/command_line.scala
--- a/src/Pure/System/command_line.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/System/command_line.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -30,7 +30,7 @@
       catch {
         case exn: Throwable =>
           if (debug) exn.printStackTrace
-          System.err.println(Exn.error_message(exn))
+          Output.error_message(Exn.message(exn))
           Exn.return_code(exn, 2)
       }
     sys.exit(rc)
diff -r f2eb0f22589f -r 433cf57550fa src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/Tools/build.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -606,8 +606,8 @@
       timeout_request.foreach(_.cancel)
 
       if (res.rc == Exn.Interrupt.return_code) {
-        if (was_timeout) res.add_err("*** Timeout").set_rc(1)
-        else res.add_err("*** Interrupt")
+        if (was_timeout) res.add_err(Output.error_text("Timeout")).set_rc(1)
+        else res.add_err(Output.error_text("Interrupt"))
       }
       else res
     }
@@ -758,8 +758,7 @@
 
       def ignore_error(msg: String): (List[Properties.T], Double) =
       {
-        System.err.println("### Ignoring bad log file: " + path +
-          (if (msg == "") "" else "\n" + msg))
+        Output.warning("Ignoring bad log file: " + path + (if (msg == "") "" else "\n" + msg))
         (Nil, 0.0)
       }
 
@@ -902,7 +901,7 @@
 
     val results =
       if (deps.is_empty) {
-        progress.echo("### Nothing to build")
+        progress.echo(Output.warning_text("Nothing to build"))
         Map.empty[String, Result]
       }
       else loop(queue, Map.empty, Map.empty)
diff -r f2eb0f22589f -r 433cf57550fa src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/Tools/main.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -61,7 +61,8 @@
                     system_mode = system_mode, sessions = List(session)))
               }
               catch {
-                case exn: Throwable => (Exn.error_message(exn) + "\n", Exn.return_code(exn, 2))
+                case exn: Throwable =>
+                  (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
               }
 
             system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
diff -r f2eb0f22589f -r 433cf57550fa src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -289,7 +289,7 @@
                 }
                 do_cancel(serial, id)
               case None =>
-                System.err.println("send_reply: unknown serial " + serial)
+                Output.warning("send_reply: unknown serial " + serial)
             }
 
             do_reply(session, serial, answer)
diff -r f2eb0f22589f -r 433cf57550fa src/Pure/build-jars
--- a/src/Pure/build-jars	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/build-jars	Tue Apr 29 13:32:13 2014 +0200
@@ -25,6 +25,7 @@
   General/graphics_file.scala
   General/linear_set.scala
   General/multi_map.scala
+  General/output.scala
   General/path.scala
   General/position.scala
   General/pretty.scala
diff -r f2eb0f22589f -r 433cf57550fa src/Tools/Graphview/src/graphview.scala
--- a/src/Tools/Graphview/src/graphview.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Tools/Graphview/src/graphview.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -34,7 +34,7 @@
           case _ => error("Bad arguments:\n" + cat_lines(args))
         }
       }
-      catch { case exn: Throwable => println(Exn.error_message(exn)); sys.exit(1) }
+      catch { case exn: Throwable => Output.error_message(Exn.message(exn)); sys.exit(1) }
 
     val top = new MainFrame {
       iconImage = GUI.isabelle_image()
diff -r f2eb0f22589f -r 433cf57550fa src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -124,7 +124,7 @@
             {
               parent.parent match {
                 case None =>
-                  System.err.println("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
+                  Output.error_message("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
                 case Some(tree) =>
                   tree.children -= head.parent
                   walk_trace(tail, lookup) // FIXME discard from lookup
@@ -140,7 +140,7 @@
             }
 
           case None =>
-            System.err.println("Simplifier_Trace_Window: unknown parent " + head.parent)
+            Output.error_message("Simplifier_Trace_Window: unknown parent " + head.parent)
         }
     }