moved Pure/Tools/isabelle_syntax.scala to Pure/System/isabelle_syntax.scala;
renamed object IsabelleSyntax to Isabelle_Syntax;

--- a/src/Pure/IsaMakefile	Fri Aug 28 21:44:48 2009 +0200
+++ b/src/Pure/IsaMakefile	Sat Aug 29 10:50:04 2009 +0200
@@ -122,10 +122,9 @@
   General/symbol.scala General/xml.scala General/yxml.scala		\
   Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala	\
   System/cygwin.scala System/gui_setup.scala				\
-  System/isabelle_process.scala System/isabelle_system.scala		\
-  System/platform.scala Thy/completion.scala Thy/thy_header.scala	\
-  Tools/isabelle_syntax.scala
-
+  System/isabelle_process.scala System/isabelle_syntax.scala		\
+  System/isabelle_system.scala System/platform.scala			\
+  Thy/completion.scala Thy/thy_header.scala \
 
 JAR_DIR = $(ISABELLE_HOME)/lib/classes
 PURE_JAR = $(JAR_DIR)/Pure.jar

--- a/src/Pure/Isar/isar.scala	Fri Aug 28 21:44:48 2009 +0200
+++ b/src/Pure/Isar/isar.scala	Sat Aug 29 10:50:04 2009 +0200
@@ -14,13 +14,13 @@
   /* basic editor commands */
 
   def create_command(id: String, text: String) =
-    output_sync("Isar.command " + IsabelleSyntax.encode_string(id) + " " +
-      IsabelleSyntax.encode_string(text))
+    output_sync("Isar.command " + Isabelle_Syntax.encode_string(id) + " " +
+      Isabelle_Syntax.encode_string(text))
 
   def insert_command(prev: String, id: String) =
-    output_sync("Isar.insert " + IsabelleSyntax.encode_string(prev) + " " +
-      IsabelleSyntax.encode_string(id))
+    output_sync("Isar.insert " + Isabelle_Syntax.encode_string(prev) + " " +
+      Isabelle_Syntax.encode_string(id))
 
   def remove_command(id: String) =
-    output_sync("Isar.remove " + IsabelleSyntax.encode_string(id))
+    output_sync("Isar.remove " + Isabelle_Syntax.encode_string(id))
 }

--- a/src/Pure/Isar/isar_document.scala	Fri Aug 28 21:44:48 2009 +0200
+++ b/src/Pure/Isar/isar_document.scala	Sat Aug 29 10:50:04 2009 +0200
@@ -22,20 +22,20 @@
   /* commands */
 
   def define_command(id: Command_ID, text: String) {
-    output_sync("Isar.define_command " + IsabelleSyntax.encode_string(id) + " " +
-      IsabelleSyntax.encode_string(text))
+    output_sync("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
+      Isabelle_Syntax.encode_string(text))
   }
 
 
   /* documents */
 
   def begin_document(id: Document_ID, path: String) {
-    output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " +
-      IsabelleSyntax.encode_string(path))
+    output_sync("Isar.begin_document " + Isabelle_Syntax.encode_string(id) + " " +
+      Isabelle_Syntax.encode_string(path))
   }
 
   def end_document(id: Document_ID) {
-    output_sync("Isar.end_document " + IsabelleSyntax.encode_string(id))
+    output_sync("Isar.end_document " + Isabelle_Syntax.encode_string(id))
   }
 
   def edit_document(old_id: Document_ID, new_id: Document_ID,
@@ -44,21 +44,21 @@
     def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
     {
       edit match {
-        case (id, None) => IsabelleSyntax.append_string(id, result)
+        case (id, None) => Isabelle_Syntax.append_string(id, result)
         case (id, Some(id2)) =>
-          IsabelleSyntax.append_string(id, result)
+          Isabelle_Syntax.append_string(id, result)
           result.append(" ")
-          IsabelleSyntax.append_string(id2, result)
+          Isabelle_Syntax.append_string(id2, result)
       }
     }
 
     val buf = new StringBuilder(40)
     buf.append("Isar.edit_document ")
-    IsabelleSyntax.append_string(old_id, buf)
+    Isabelle_Syntax.append_string(old_id, buf)
     buf.append(" ")
-    IsabelleSyntax.append_string(new_id, buf)
+    Isabelle_Syntax.append_string(new_id, buf)
     buf.append(" ")
-    IsabelleSyntax.append_list(append_edit, edits, buf)
+    Isabelle_Syntax.append_list(append_edit, edits, buf)
     output_sync(buf.toString)
   }
 }

--- a/src/Pure/System/isabelle_process.scala	Fri Aug 28 21:44:48 2009 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sat Aug 29 10:50:04 2009 +0200
@@ -204,14 +204,14 @@
 
 
   def command(text: String) =
-    output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
+    output_sync("Isabelle.command " + Isabelle_Syntax.encode_string(text))
 
   def command(props: List[(String, String)], text: String) =
-    output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
-      IsabelleSyntax.encode_string(text))
+    output_sync("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
+      Isabelle_Syntax.encode_string(text))
 
   def ML(text: String) =
-    output_sync("ML_val " + IsabelleSyntax.encode_string(text))
+    output_sync("ML_val " + Isabelle_Syntax.encode_string(text))
 
   def close() = synchronized {    // FIXME watchdog/timeout
     output_raw("\u0000")

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_syntax.scala	Sat Aug 29 10:50:04 2009 +0200
@@ -0,0 +1,74 @@
+/*  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
+  }
+}

--- a/src/Pure/Tools/isabelle_syntax.scala	Fri Aug 28 21:44:48 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-/*  Title:      Pure/Tools/isabelle_syntax.scala
-    Author:     Makarius
-
-Isabelle outer syntax.
-*/
-
-package isabelle
-
-
-object IsabelleSyntax {
-
-  /* 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
-  }
-}