Scala wrapper for interactive Isar documents;

--- a/src/Pure/IsaMakefile	Sun Jan 18 20:05:01 2009 +0100
+++ b/src/Pure/IsaMakefile	Sun Jan 18 20:06:51 2009 +0100
@@ -126,9 +126,9 @@
 SCALA_FILES = General/event_bus.scala General/markup.scala		\
   General/position.scala General/swing.scala General/symbol.scala	\
   General/xml.scala General/yxml.scala Isar/isar.scala			\
-  Isar/outer_keyword.scala Thy/thy_header.scala				\
-  Tools/isabelle_process.scala Tools/isabelle_syntax.scala		\
-  Tools/isabelle_system.scala
+  Isar/isar_document.scala Isar/outer_keyword.scala			\
+  Thy/thy_header.scala Tools/isabelle_process.scala			\
+  Tools/isabelle_syntax.scala Tools/isabelle_system.scala
 
 
 SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/isar_document.scala	Sun Jan 18 20:06:51 2009 +0100
@@ -0,0 +1,61 @@
+/*  Title:      Pure/Isar/isar_document.scala
+    Author:     Makarius
+
+Interactive Isar documents.
+*/
+
+package isabelle
+
+
+object IsarDocument
+{
+  /* unique identifiers */
+
+  type State_ID = String
+  type Command_ID = String
+  type Document_ID = String
+
+
+  /* commands */
+
+  def define_command(proc: IsabelleProcess, id: Command_ID, text: String) {
+    proc.output_sync("Isar.define_command " + IsabelleSyntax.encode_string(id) + " " +
+      IsabelleSyntax.encode_string(text))
+  }
+
+
+  /* documents */
+
+  def begin_document(proc: IsabelleProcess, id: Document_ID, path: String) {
+    proc.output_sync("Isar.begin_document " + IsabelleSyntax.encode_string(id) + " " +
+       IsabelleSyntax.encode_string(path))
+  }
+
+  def end_document(proc: IsabelleProcess, id: Document_ID) {
+    proc.output_sync("Isar.end_document " + IsabelleSyntax.encode_string(id))
+  }
+
+  def edit_document(proc: IsabelleProcess, old_id: Document_ID, new_id: Document_ID,
+      edits: List[(Command_ID, Option[Command_ID])])
+  {
+    def append_edit(edit: (Command_ID, Option[Command_ID]), result: StringBuilder)
+    {
+      edit match {
+        case (id, None) => IsabelleSyntax.append_string(id, result)
+        case (id, Some(id2)) =>
+          IsabelleSyntax.append_string(id, result)
+          result.append(" ")
+          IsabelleSyntax.append_string(id2, result)
+      }
+    }
+
+    val buf = new StringBuilder(40)
+    buf.append("Isar.edit_document ")
+    IsabelleSyntax.append_string(old_id, buf)
+    buf.append(" ")
+    IsabelleSyntax.append_string(new_id, buf)
+    buf.append(" ")
+    IsabelleSyntax.append_list(append_edit, edits, buf)
+    proc.output_sync(buf.toString)
+  }
+}