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);
     1 /*  Title:      Pure/System/isabelle_syntax.scala
     2     Author:     Makarius
     3 
     4 Isabelle outer syntax.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Isabelle_Syntax
    11 {
    12   /* string token */
    13 
    14   def append_string(str: String, result: StringBuilder)
    15   {
    16     result.append("\"")
    17     for (c <- str) {
    18       if (c < 32 || c == '\\' || c == '\"') {
    19         result.append("\\")
    20         if (c < 10) result.append('0')
    21         if (c < 100) result.append('0')
    22         result.append(c.asInstanceOf[Int].toString)
    23       }
    24       else result.append(c)
    25     }
    26     result.append("\"")
    27   }
    28 
    29   def encode_string(str: String) =
    30   {
    31     val result = new StringBuilder(str.length + 10)
    32     append_string(str, result)
    33     result.toString
    34   }
    35 
    36 
    37   /* list */
    38 
    39   def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A],
    40     result: StringBuilder)
    41   {
    42     result.append("(")
    43     val elems = body.iterator
    44     if (elems.hasNext) append_elem(elems.next, result)
    45     while (elems.hasNext) {
    46       result.append(", ")
    47       append_elem(elems.next, result)
    48     }
    49     result.append(")")
    50   }
    51 
    52   def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
    53   {
    54     val result = new StringBuilder
    55     append_list(append_elem, elems, result)
    56     result.toString
    57   }
    58 
    59 
    60   /* properties */
    61 
    62   def append_properties(props: List[(String, String)], result: StringBuilder)
    63   {
    64     append_list((p: (String, String), res) =>
    65       { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result)
    66   }
    67 
    68   def encode_properties(props: List[(String, String)]) =
    69   {
    70     val result = new StringBuilder
    71     append_properties(props, result)
    72     result.toString
    73   }
    74 }