more systematic Isabelle output, like in classic Isabelle/ML (without markup);
authorwenzelm
Tue Apr 29 13:32:13 2014 +0200 (2014-04-29)
changeset 56782433cf57550fa
parent 56781 f2eb0f22589f
child 56783 afaec818fcfd
more systematic Isabelle output, like in classic Isabelle/ML (without markup);
src/Pure/Concurrent/consumer_thread.scala
src/Pure/General/completion.scala
src/Pure/General/exn.scala
src/Pure/General/output.scala
src/Pure/General/timing.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/session.scala
src/Pure/System/command_line.scala
src/Pure/Tools/build.scala
src/Pure/Tools/main.scala
src/Pure/Tools/simplifier_trace.scala
src/Pure/build-jars
src/Tools/Graphview/src/graphview.scala
src/Tools/jEdit/src/simplifier_trace_window.scala
     1.1 --- a/src/Pure/Concurrent/consumer_thread.scala	Tue Apr 29 13:29:05 2014 +0200
     1.2 +++ b/src/Pure/Concurrent/consumer_thread.scala	Tue Apr 29 13:32:13 2014 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    def is_active: Boolean = active && thread.isAlive
     1.5  
     1.6    private def failure(exn: Throwable): Unit =
     1.7 -    System.err.println(
     1.8 +    Output.error_message(
     1.9        "Consumer thread failure: " + quote(thread.getName) + "\n" + Exn.message(exn))
    1.10  
    1.11    private def robust_finish(): Unit =
     2.1 --- a/src/Pure/General/completion.scala	Tue Apr 29 13:29:05 2014 +0200
     2.2 +++ b/src/Pure/General/completion.scala	Tue Apr 29 13:32:13 2014 +0200
     2.3 @@ -62,7 +62,7 @@
     2.4      def load(): History =
     2.5      {
     2.6        def ignore_error(msg: String): Unit =
     2.7 -        System.err.println("### Ignoring bad content of file " + COMPLETION_HISTORY +
     2.8 +        Output.warning("Ignoring bad content of file " + COMPLETION_HISTORY +
     2.9            (if (msg == "") "" else "\n" + msg))
    2.10  
    2.11        val content =
     3.1 --- a/src/Pure/General/exn.scala	Tue Apr 29 13:29:05 2014 +0200
     3.2 +++ b/src/Pure/General/exn.scala	Tue Apr 29 13:32:13 2014 +0200
     3.3 @@ -73,11 +73,5 @@
     3.4  
     3.5    def message(exn: Throwable): String =
     3.6      user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
     3.7 -
     3.8 -
     3.9 -  /* TTY error message */
    3.10 -
    3.11 -  def error_message(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
    3.12 -  def error_message(exn: Throwable): String = error_message(message(exn))
    3.13  }
    3.14  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/General/output.scala	Tue Apr 29 13:32:13 2014 +0200
     4.3 @@ -0,0 +1,18 @@
     4.4 +/*  Title:      Pure/General/output.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Isabelle output channels: plain text without markup.
     4.8 +*/
     4.9 +
    4.10 +package isabelle
    4.11 +
    4.12 +
    4.13 +object Output
    4.14 +{
    4.15 +  def warning_text(msg: String): String = cat_lines(split_lines(msg).map("### " + _))
    4.16 +  def error_text(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
    4.17 +
    4.18 +  def warning(msg: String) { System.err.println(warning_text(msg)) }
    4.19 +  def error_message(msg: String) { System.err.println(error_text(msg)) }
    4.20 +}
    4.21 +
     5.1 --- a/src/Pure/General/timing.scala	Tue Apr 29 13:29:05 2014 +0200
     5.2 +++ b/src/Pure/General/timing.scala	Tue Apr 29 13:32:13 2014 +0200
     5.3 @@ -20,7 +20,7 @@
     5.4  
     5.5        val timing = stop - start
     5.6        if (timing.is_relevant)
     5.7 -        System.err.println(
     5.8 +        Output.warning(
     5.9            (if (message == null || message.isEmpty) "" else message + ": ") +
    5.10              timing.message + " elapsed time")
    5.11  
     6.1 --- a/src/Pure/PIDE/command.scala	Tue Apr 29 13:29:05 2014 +0200
     6.2 +++ b/src/Pure/PIDE/command.scala	Tue Apr 29 13:32:13 2014 +0200
     6.3 @@ -179,14 +179,14 @@
     6.4                    add_status(markup).
     6.5                    add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem))
     6.6                case _ =>
     6.7 -                System.err.println("Ignored status message: " + msg)
     6.8 +                Output.warning("Ignored status message: " + msg)
     6.9                  state
    6.10              })
    6.11  
    6.12          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
    6.13            (this /: msgs)((state, msg) =>
    6.14              {
    6.15 -              def bad(): Unit = System.err.println("Ignored report message: " + msg)
    6.16 +              def bad(): Unit = Output.warning("Ignored report message: " + msg)
    6.17  
    6.18                msg match {
    6.19                  case XML.Elem(
    6.20 @@ -238,7 +238,7 @@
    6.21                st
    6.22  
    6.23              case _ =>
    6.24 -              System.err.println("Ignored message without serial number: " + message)
    6.25 +              Output.warning("Ignored message without serial number: " + message)
    6.26                this
    6.27            }
    6.28      }
     7.1 --- a/src/Pure/PIDE/markup_tree.scala	Tue Apr 29 13:29:05 2014 +0200
     7.2 +++ b/src/Pure/PIDE/markup_tree.scala	Tue Apr 29 13:32:13 2014 +0200
     7.3 @@ -153,7 +153,7 @@
     7.4            if (body.forall(e => new_range.contains(e._1)))
     7.5              new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
     7.6            else {
     7.7 -            System.err.println("Ignored overlapping markup information: " + new_markup +
     7.8 +            Output.warning("Ignored overlapping markup information: " + new_markup +
     7.9                body.filter(e => !new_range.contains(e._1)).mkString("\n"))
    7.10              this
    7.11            }
     8.1 --- a/src/Pure/PIDE/session.scala	Tue Apr 29 13:29:05 2014 +0200
     8.2 +++ b/src/Pure/PIDE/session.scala	Tue Apr 29 13:32:13 2014 +0200
     8.3 @@ -37,7 +37,7 @@
     8.4            try { c.consume(a) }
     8.5            catch {
     8.6              case exn: Throwable =>
     8.7 -              System.err.println("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
     8.8 +              Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn))
     8.9            })
    8.10        }
    8.11      }
    8.12 @@ -115,7 +115,7 @@
    8.13        val (handlers1, functions1) =
    8.14          handlers.get(name) match {
    8.15            case Some(old_handler) =>
    8.16 -            System.err.println("Redefining protocol handler: " + name)
    8.17 +            Output.warning("Redefining protocol handler: " + name)
    8.18              old_handler.stop(prover)
    8.19              (handlers - name, functions -- old_handler.functions.keys)
    8.20            case None => (handlers, functions)
    8.21 @@ -135,8 +135,8 @@
    8.22          }
    8.23          catch {
    8.24            case exn: Throwable =>
    8.25 -            System.err.println(Exn.error_message(
    8.26 -              "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn)))
    8.27 +            Output.error_message(
    8.28 +              "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
    8.29              (handlers1, functions1)
    8.30          }
    8.31  
    8.32 @@ -149,8 +149,8 @@
    8.33            try { functions(a)(msg) }
    8.34            catch {
    8.35              case exn: Throwable =>
    8.36 -              System.err.println(Exn.error_message(
    8.37 -                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn)))
    8.38 +              Output.error_message(
    8.39 +                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
    8.40              false
    8.41            }
    8.42          case _ => false
    8.43 @@ -381,7 +381,7 @@
    8.44                global_state.change(_.define_blob(digest))
    8.45                prover.get.define_blob(digest, blob.bytes)
    8.46              case None =>
    8.47 -              System.err.println("Missing blob for SHA1 digest " + digest)
    8.48 +              Output.error_message("Missing blob for SHA1 digest " + digest)
    8.49            }
    8.50          }
    8.51  
    8.52 @@ -411,7 +411,7 @@
    8.53        def bad_output()
    8.54        {
    8.55          if (verbose)
    8.56 -          System.err.println("Ignoring bad prover output: " + output.message.toString)
    8.57 +          Output.warning("Ignoring bad prover output: " + output.message.toString)
    8.58        }
    8.59  
    8.60        def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
     9.1 --- a/src/Pure/System/command_line.scala	Tue Apr 29 13:29:05 2014 +0200
     9.2 +++ b/src/Pure/System/command_line.scala	Tue Apr 29 13:32:13 2014 +0200
     9.3 @@ -30,7 +30,7 @@
     9.4        catch {
     9.5          case exn: Throwable =>
     9.6            if (debug) exn.printStackTrace
     9.7 -          System.err.println(Exn.error_message(exn))
     9.8 +          Output.error_message(Exn.message(exn))
     9.9            Exn.return_code(exn, 2)
    9.10        }
    9.11      sys.exit(rc)
    10.1 --- a/src/Pure/Tools/build.scala	Tue Apr 29 13:29:05 2014 +0200
    10.2 +++ b/src/Pure/Tools/build.scala	Tue Apr 29 13:32:13 2014 +0200
    10.3 @@ -606,8 +606,8 @@
    10.4        timeout_request.foreach(_.cancel)
    10.5  
    10.6        if (res.rc == Exn.Interrupt.return_code) {
    10.7 -        if (was_timeout) res.add_err("*** Timeout").set_rc(1)
    10.8 -        else res.add_err("*** Interrupt")
    10.9 +        if (was_timeout) res.add_err(Output.error_text("Timeout")).set_rc(1)
   10.10 +        else res.add_err(Output.error_text("Interrupt"))
   10.11        }
   10.12        else res
   10.13      }
   10.14 @@ -758,8 +758,7 @@
   10.15  
   10.16        def ignore_error(msg: String): (List[Properties.T], Double) =
   10.17        {
   10.18 -        System.err.println("### Ignoring bad log file: " + path +
   10.19 -          (if (msg == "") "" else "\n" + msg))
   10.20 +        Output.warning("Ignoring bad log file: " + path + (if (msg == "") "" else "\n" + msg))
   10.21          (Nil, 0.0)
   10.22        }
   10.23  
   10.24 @@ -902,7 +901,7 @@
   10.25  
   10.26      val results =
   10.27        if (deps.is_empty) {
   10.28 -        progress.echo("### Nothing to build")
   10.29 +        progress.echo(Output.warning_text("Nothing to build"))
   10.30          Map.empty[String, Result]
   10.31        }
   10.32        else loop(queue, Map.empty, Map.empty)
    11.1 --- a/src/Pure/Tools/main.scala	Tue Apr 29 13:29:05 2014 +0200
    11.2 +++ b/src/Pure/Tools/main.scala	Tue Apr 29 13:32:13 2014 +0200
    11.3 @@ -61,7 +61,8 @@
    11.4                      system_mode = system_mode, sessions = List(session)))
    11.5                }
    11.6                catch {
    11.7 -                case exn: Throwable => (Exn.error_message(exn) + "\n", Exn.return_code(exn, 2))
    11.8 +                case exn: Throwable =>
    11.9 +                  (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
   11.10                }
   11.11  
   11.12              system_dialog.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
    12.1 --- a/src/Pure/Tools/simplifier_trace.scala	Tue Apr 29 13:29:05 2014 +0200
    12.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Tue Apr 29 13:32:13 2014 +0200
    12.3 @@ -289,7 +289,7 @@
    12.4                  }
    12.5                  do_cancel(serial, id)
    12.6                case None =>
    12.7 -                System.err.println("send_reply: unknown serial " + serial)
    12.8 +                Output.warning("send_reply: unknown serial " + serial)
    12.9              }
   12.10  
   12.11              do_reply(session, serial, answer)
    13.1 --- a/src/Pure/build-jars	Tue Apr 29 13:29:05 2014 +0200
    13.2 +++ b/src/Pure/build-jars	Tue Apr 29 13:32:13 2014 +0200
    13.3 @@ -25,6 +25,7 @@
    13.4    General/graphics_file.scala
    13.5    General/linear_set.scala
    13.6    General/multi_map.scala
    13.7 +  General/output.scala
    13.8    General/path.scala
    13.9    General/position.scala
   13.10    General/pretty.scala
    14.1 --- a/src/Tools/Graphview/src/graphview.scala	Tue Apr 29 13:29:05 2014 +0200
    14.2 +++ b/src/Tools/Graphview/src/graphview.scala	Tue Apr 29 13:32:13 2014 +0200
    14.3 @@ -34,7 +34,7 @@
    14.4            case _ => error("Bad arguments:\n" + cat_lines(args))
    14.5          }
    14.6        }
    14.7 -      catch { case exn: Throwable => println(Exn.error_message(exn)); sys.exit(1) }
    14.8 +      catch { case exn: Throwable => Output.error_message(Exn.message(exn)); sys.exit(1) }
    14.9  
   14.10      val top = new MainFrame {
   14.11        iconImage = GUI.isabelle_image()
    15.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Apr 29 13:29:05 2014 +0200
    15.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Apr 29 13:32:13 2014 +0200
    15.3 @@ -124,7 +124,7 @@
    15.4              {
    15.5                parent.parent match {
    15.6                  case None =>
    15.7 -                  System.err.println("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
    15.8 +                  Output.error_message("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
    15.9                  case Some(tree) =>
   15.10                    tree.children -= head.parent
   15.11                    walk_trace(tail, lookup) // FIXME discard from lookup
   15.12 @@ -140,7 +140,7 @@
   15.13              }
   15.14  
   15.15            case None =>
   15.16 -            System.err.println("Simplifier_Trace_Window: unknown parent " + head.parent)
   15.17 +            Output.error_message("Simplifier_Trace_Window: unknown parent " + head.parent)
   15.18          }
   15.19      }
   15.20