src/Pure/General/output.scala
author wenzelm
Sun, 14 May 2017 17:05:06 +0200
changeset 65828 02dd430d80c5
parent 64370 865b39487b5d
child 67178 70576478bda9
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
57453
77d13a98f1c8 clarified quasi-generic PIDE;
wenzelm
parents: 56831
diff changeset
     1
/*  Title:      Pure/General/output.scala
56782
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
     3
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62553
diff changeset
     4
Isabelle output channels.
56782
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
     5
*/
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
     6
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
     7
package isabelle
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
     8
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
     9
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
    10
object Output
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
    11
{
59671
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents: 57453
diff changeset
    12
  def clean_yxml(msg: String): String =
62938
79f41fbdf74a clean message more thoroughly;
wenzelm
parents: 62930
diff changeset
    13
    try { XML.content(Protocol_Message.clean_reports(YXML.parse_body(msg))) }
59671
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents: 57453
diff changeset
    14
    catch { case ERROR(_) => msg }
56782
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
    15
59671
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents: 57453
diff changeset
    16
  def writeln_text(msg: String): String = clean_yxml(msg)
65828
02dd430d80c5 tuned signature;
wenzelm
parents: 64370
diff changeset
    17
02dd430d80c5 tuned signature;
wenzelm
parents: 64370
diff changeset
    18
  def warning_text(msg: String): String =
02dd430d80c5 tuned signature;
wenzelm
parents: 64370
diff changeset
    19
    cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
02dd430d80c5 tuned signature;
wenzelm
parents: 64370
diff changeset
    20
02dd430d80c5 tuned signature;
wenzelm
parents: 64370
diff changeset
    21
  def error_message_text(msg: String): String =
02dd430d80c5 tuned signature;
wenzelm
parents: 64370
diff changeset
    22
    cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
59671
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents: 57453
diff changeset
    23
62553
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    24
  def writeln(msg: String, stdout: Boolean = false)
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    25
  {
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    26
    if (msg != "") {
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    27
      if (stdout) Console.println(writeln_text(msg))
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    28
      else Console.err.println(writeln_text(msg))
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    29
    }
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    30
  }
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    31
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    32
  def warning(msg: String, stdout: Boolean = false)
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    33
  {
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    34
    if (msg != "") {
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    35
      if (stdout) Console.println(warning_text(msg))
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    36
      else Console.err.println(warning_text(msg))
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    37
    }
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    38
  }
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    39
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    40
  def error_message(msg: String, stdout: Boolean = false)
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    41
  {
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    42
    if (msg != "") {
65828
02dd430d80c5 tuned signature;
wenzelm
parents: 64370
diff changeset
    43
      if (stdout) Console.println(error_message_text(msg))
02dd430d80c5 tuned signature;
wenzelm
parents: 64370
diff changeset
    44
      else Console.err.println(error_message_text(msg))
62553
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    45
    }
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    46
  }
56782
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
    47
}