# HG changeset patch
# User wenzelm
# Date 1219504972 -7200
# Node ID 8adddc0b591f60ed1cc39f59a9032080071345a7
# Parent  dbb93a5e6e6a48aa424b9b36f8708381b4fd0d15
Isabelle outer syntax.

diff -r dbb93a5e6e6a -r 8adddc0b591f src/Pure/Tools/isabelle_syntax.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/isabelle_syntax.scala	Sat Aug 23 17:22:52 2008 +0200
@@ -0,0 +1,56 @@
+/*  Title:      Pure/Tools/isabelle_syntax.scala
+    ID:         $Id$
+    Author:     Makarius
+
+Isabelle outer syntax.
+*/
+
+package isabelle
+
+import java.util.{Properties, Enumeration}
+
+
+object IsabelleSyntax {
+
+  /* string token */
+
+  def append_string(str: String, result: StringBuilder) = {
+    result.append("\"")
+    for (c <- str) {
+      if (c < 32 || c == '\\' || c == '\"') {
+        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 + 20)
+    append_string(str, result)
+    result.toString
+  }
+
+
+  /* properties */
+
+  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)
+      if (names.hasMoreElements) result.append(", ")
+    }
+    result.append(")")
+  }
+
+  def encode_properties(props: Properties) = {
+    val result = new StringBuilder(40)
+    append_properties(props, result)
+    result.toString
+  }
+
+}