src/Pure/General/output.scala
author wenzelm
Sat, 09 Apr 2016 16:16:05 +0200
changeset 62930 51ac6bc389e8
parent 62553 d2e0d626fb96
child 62938 79f41fbdf74a
permissions -rw-r--r--
shared output primitives of physical/virtual Pure;
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
77d13a98f1c8 clarified quasi-generic PIDE;
wenzelm
parents: 56831
diff changeset
     2
    Module:     PIDE
56782
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
     4
62930
51ac6bc389e8 shared output primitives of physical/virtual Pure;
wenzelm
parents: 62553
diff changeset
     5
Isabelle output channels.
56782
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
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
     8
package isabelle
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
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
    11
object Output
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
    12
{
59671
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents: 57453
diff changeset
    13
  def clean_yxml(msg: String): String =
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents: 57453
diff changeset
    14
    try { XML.content(YXML.parse_body(msg)) }
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents: 57453
diff changeset
    15
    catch { case ERROR(_) => msg }
56782
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
    16
59671
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents: 57453
diff changeset
    17
  def writeln_text(msg: String): String = clean_yxml(msg)
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents: 57453
diff changeset
    18
  def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents: 57453
diff changeset
    19
  def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
wenzelm
parents: 57453
diff changeset
    20
62553
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    21
  def writeln(msg: String, stdout: Boolean = false)
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    22
  {
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    23
    if (msg != "") {
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    24
      if (stdout) Console.println(writeln_text(msg))
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    25
      else Console.err.println(writeln_text(msg))
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    26
    }
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    27
  }
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    28
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    29
  def warning(msg: String, stdout: Boolean = false)
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    30
  {
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    31
    if (msg != "") {
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    32
      if (stdout) Console.println(warning_text(msg))
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    33
      else Console.err.println(warning_text(msg))
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    34
    }
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    35
  }
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    36
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    37
  def error_message(msg: String, stdout: Boolean = false)
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    38
  {
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    39
    if (msg != "") {
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    40
      if (stdout) Console.println(error_text(msg))
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    41
      else Console.err.println(error_text(msg))
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    42
    }
d2e0d626fb96 tuned signature;
wenzelm
parents: 62297
diff changeset
    43
  }
56782
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents:
diff changeset
    44
}