src/Pure/Tools/isabelle_syntax.scala

 
 object IsabelleSyntax {
 
   /* string token */
 
-  def append_string(str: String, result: StringBuilder) = {
+  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')

       else result.append(c)
     }
     result.append("\"")
   }
 
-  def encode_string(str: String) = {
+  def encode_string(str: String) =
+  {
     val result = new StringBuilder(str.length + 20)
     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(20)
+    append_list(append_elem, elems, result)
+    result.toString
+  }
+
+
   /* properties */
 
-  def append_properties(props: Properties, result: StringBuilder) = {
+  def append_properties(props: Properties, result: StringBuilder)
+  {
     result.append("(")
     val names = props.propertyNames.asInstanceOf[Enumeration[String]]
     while (names.hasMoreElements) {
       val name = names.nextElement; val value = props.getProperty(name)
       append_string(name, result); result.append(" = "); append_string(value, result)