src/Pure/System/isabelle_syntax.scala

+/*  Title:      Pure/System/isabelle_syntax.scala
+    Author:     Makarius
+
+Isabelle outer syntax.
+*/
+
+package isabelle
+
+
+object Isabelle_Syntax
+{
+  /* string token */
+
+  def append_string(str: String, result: StringBuilder)
+  {
+    result.append("\"")
+    for (c <- str) {
+      if (c < 32 || c == '\\' || c == '\"') {
+        result.append("\\")
+        if (c < 10) result.append('0')
+        if (c < 100) result.append('0')
+        result.append(c.asInstanceOf[Int].toString)
+      }
+      else result.append(c)
+    }
+    result.append("\"")
+  }
+
+  def encode_string(str: String) =
+  {
+    val result = new StringBuilder(str.length + 10)
+    append_string(str, result)
+    result.toString
+  }
+
+
+  /* list */
+
+  def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A],
+    result: StringBuilder)
+  {
+    result.append("(")
+    val elems = body.elements
+    if (elems.hasNext) append_elem(elems.next, result)
+    while (elems.hasNext) {
+      result.append(", ")
+      append_elem(elems.next, result)
+    }
+    result.append(")")
+  }
+
+  def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
+  {
+    val result = new StringBuilder
+    append_list(append_elem, elems, result)
+    result.toString
+  }
+
+
+  /* properties */
+
+  def append_properties(props: List[(String, String)], result: StringBuilder)
+  {
+    append_list((p: (String, String), res) =>
+      { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result)
+  }
+
+  def encode_properties(props: List[(String, String)]) =
+  {
+    val result = new StringBuilder
+    append_properties(props, result)
+    result.toString
+  }
+}