src/Pure/System/isabelle_syntax.scala
author wenzelm
Wed Jun 02 11:09:26 2010 +0200 (2010-06-02 ago)
changeset 37251 72c7e636067b
parent 36011 3ff725ac13a4
child 43770 88b1b883e8d8
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
wenzelm@32448
     1
/*  Title:      Pure/System/isabelle_syntax.scala
wenzelm@27951
     2
    Author:     Makarius
wenzelm@27951
     3
wenzelm@27951
     4
Isabelle outer syntax.
wenzelm@27951
     5
*/
wenzelm@27951
     6
wenzelm@27951
     7
package isabelle
wenzelm@27951
     8
wenzelm@27951
     9
wenzelm@32448
    10
object Isabelle_Syntax
wenzelm@32448
    11
{
wenzelm@27951
    12
  /* string token */
wenzelm@27951
    13
wenzelm@29552
    14
  def append_string(str: String, result: StringBuilder)
wenzelm@29552
    15
  {
wenzelm@27951
    16
    result.append("\"")
wenzelm@27951
    17
    for (c <- str) {
wenzelm@27951
    18
      if (c < 32 || c == '\\' || c == '\"') {
wenzelm@27954
    19
        result.append("\\")
wenzelm@27951
    20
        if (c < 10) result.append('0')
wenzelm@27951
    21
        if (c < 100) result.append('0')
wenzelm@27951
    22
        result.append(c.asInstanceOf[Int].toString)
wenzelm@27951
    23
      }
wenzelm@27951
    24
      else result.append(c)
wenzelm@27951
    25
    }
wenzelm@27951
    26
    result.append("\"")
wenzelm@27951
    27
  }
wenzelm@27951
    28
wenzelm@29552
    29
  def encode_string(str: String) =
wenzelm@29552
    30
  {
wenzelm@29571
    31
    val result = new StringBuilder(str.length + 10)
wenzelm@27951
    32
    append_string(str, result)
wenzelm@27951
    33
    result.toString
wenzelm@27951
    34
  }
wenzelm@27951
    35
wenzelm@27951
    36
wenzelm@29552
    37
  /* list */
wenzelm@29552
    38
wenzelm@29552
    39
  def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A],
wenzelm@29552
    40
    result: StringBuilder)
wenzelm@29552
    41
  {
wenzelm@29552
    42
    result.append("(")
wenzelm@36011
    43
    val elems = body.iterator
wenzelm@29552
    44
    if (elems.hasNext) append_elem(elems.next, result)
wenzelm@29552
    45
    while (elems.hasNext) {
wenzelm@29552
    46
      result.append(", ")
wenzelm@29552
    47
      append_elem(elems.next, result)
wenzelm@29552
    48
    }
wenzelm@29552
    49
    result.append(")")
wenzelm@29552
    50
  }
wenzelm@29552
    51
wenzelm@29552
    52
  def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
wenzelm@29552
    53
  {
wenzelm@29571
    54
    val result = new StringBuilder
wenzelm@29552
    55
    append_list(append_elem, elems, result)
wenzelm@29552
    56
    result.toString
wenzelm@29552
    57
  }
wenzelm@29552
    58
wenzelm@29552
    59
wenzelm@27951
    60
  /* properties */
wenzelm@27951
    61
wenzelm@29571
    62
  def append_properties(props: List[(String, String)], result: StringBuilder)
wenzelm@29552
    63
  {
wenzelm@29571
    64
    append_list((p: (String, String), res) =>
wenzelm@29571
    65
      { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result)
wenzelm@27951
    66
  }
wenzelm@27951
    67
wenzelm@29571
    68
  def encode_properties(props: List[(String, String)]) =
wenzelm@29571
    69
  {
wenzelm@29571
    70
    val result = new StringBuilder
wenzelm@27951
    71
    append_properties(props, result)
wenzelm@27951
    72
    result.toString
wenzelm@27951
    73
  }
wenzelm@27951
    74
}