Isar_Document command input via native Isabelle_Process commands, using YXML and XML_Data representation;

--- a/src/Pure/Isar/isar_document.ML	Wed Aug 11 00:44:48 2010 +0200
+++ b/src/Pure/Isar/isar_document.ML	Wed Aug 11 00:46:07 2010 +0200
@@ -143,10 +143,16 @@
 
 in
 
-fun define_command (id: Document.command_id) tr =
-  NAMED_CRITICAL "Isar" (fn () =>
-    Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
-      handle Symtab.DUP dup => err_dup "command" dup);
+fun define_command (id: Document.command_id) text =
+  let
+    val tr =
+      Position.setmp_thread_data (Position.id_only id) (fn () =>
+        Outer_Syntax.prepare_command (Position.id id) text) ();
+  in
+    NAMED_CRITICAL "Isar" (fn () =>
+      Unsynchronized.change global_commands (Symtab.update_new (id, Toplevel.put_id id tr))
+        handle Symtab.DUP dup => err_dup "command" dup)
+  end;
 
 fun the_command (id: Document.command_id) =
   (case Symtab.lookup (! global_commands) id of
@@ -178,7 +184,7 @@
 
 
 
-(** main operations **)
+(** document editing **)
 
 (* execution *)
 
@@ -241,52 +247,50 @@
 in
 
 fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
-  NAMED_CRITICAL "Isar" (fn () =>
-    let
-      val old_document = the_document old_id;
-      val new_document = fold edit_nodes edits old_document;
+  Position.setmp_thread_data (Position.id_only new_id) (fn () =>
+    NAMED_CRITICAL "Isar" (fn () =>
+      let
+        val old_document = the_document old_id;
+        val new_document = fold edit_nodes edits old_document;
 
-      fun update_node name node =
-        (case first_entry (is_changed (the_node old_document name)) node of
-          NONE => ([], node)
-        | SOME (prev, id, _) =>
-            let
-              val prev_state_id = the (#state (the_entry node (the prev)));
-              val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []);
-              val node' = fold set_entry_state updates node;
-            in (rev updates, node') end);
+        fun update_node name node =
+          (case first_entry (is_changed (the_node old_document name)) node of
+            NONE => ([], node)
+          | SOME (prev, id, _) =>
+              let
+                val prev_state_id = the (#state (the_entry node (the prev)));
+                val (_, updates) = fold_entries id (new_state name o #1) node (prev_state_id, []);
+                val node' = fold set_entry_state updates node;
+              in (rev updates, node') end);
 
-      (* FIXME proper node deps *)
-      val (updatess, new_document') =
-        (Graph.keys new_document, new_document)
-          |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
+        (* FIXME proper node deps *)
+        val (updatess, new_document') =
+          (Graph.keys new_document, new_document)
+            |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
 
-      val _ = define_document new_id new_document';
-      val _ = updates_status (flat updatess);
-      val _ = execute new_document';
-    in () end);
+        val _ = define_document new_id new_document';
+        val _ = updates_status (flat updatess);
+        val _ = execute new_document';
+      in () end)) ();
 
 end;
 
 
 
-(** concrete syntax **)
+(** Isabelle process commands **)
+
+val _ =
+  Isabelle_Process.add_command "Isar_Document.define_command"
+    (fn [id, text] => define_command id text);
 
 val _ =
-  Outer_Syntax.internal_command "Isar.define_command"
-    (Parse.string -- Parse.string >> (fn (id, text) =>
-      Toplevel.position (Position.id_only id) o
-      Toplevel.imperative (fn () =>
-        define_command id (Outer_Syntax.prepare_command (Position.id id) text))));
-
-val _ =
-  Outer_Syntax.internal_command "Isar.edit_document"
-    (Parse.string -- Parse.string --
-      Parse_Value.list
-        (Parse.string -- Scan.option (Parse_Value.list (Parse.string -- Scan.option Parse.string)))
-      >> (fn ((old_id, new_id), edits) =>
-          Toplevel.position (Position.id_only new_id) o
-          Toplevel.imperative (fn () => edit_document old_id new_id edits)));
+  Isabelle_Process.add_command "Isar_Document.edit_document"
+    (fn [old_id, new_id, edits] =>
+      edit_document old_id new_id
+        (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string
+            (XML_Data.dest_option (XML_Data.dest_list
+                (XML_Data.dest_pair XML_Data.dest_string
+                  (XML_Data.dest_option XML_Data.dest_string))))) (YXML.parse_body edits)));
 
 end;
 

--- a/src/Pure/Isar/isar_document.scala	Wed Aug 11 00:44:48 2010 +0200
+++ b/src/Pure/Isar/isar_document.scala	Wed Aug 11 00:46:07 2010 +0200
@@ -37,10 +37,8 @@
 
   /* commands */
 
-  def define_command(id: Document.Command_ID, text: String) {
-    input("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
-      Isabelle_Syntax.encode_string(text))
-  }
+  def define_command(id: Document.Command_ID, text: String): Unit =
+    input("Isar_Document.define_command", id, text)
 
 
   /* documents */
@@ -48,38 +46,14 @@
   def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
       edits: List[Document.Edit[Document.Command_ID]])
   {
-    def append_edit(
-        edit: (Option[Document.Command_ID], Option[Document.Command_ID]), result: StringBuilder)
-    {
-      Isabelle_Syntax.append_string(edit._1 getOrElse Document.NO_ID, result)
-      edit._2 match {
-        case None =>
-        case Some(id2) =>
-          result.append(" ")
-          Isabelle_Syntax.append_string(id2, result)
-      }
-    }
+    def make_id1(id1: Option[Document.Command_ID]): XML.Body =
+      XML_Data.make_string(id1 getOrElse Document.NO_ID)
+    val arg =
+      XML_Data.make_list(
+        XML_Data.make_pair(XML_Data.make_string)(
+          XML_Data.make_option(XML_Data.make_list(
+              XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_string))))))(edits)
 
-    def append_node_edit(
-        edit: (String, Option[List[(Option[Document.Command_ID], Option[Document.Command_ID])]]),
-        result: StringBuilder)
-    {
-      Isabelle_Syntax.append_string(edit._1, result)
-      edit._2 match {
-        case None =>
-        case Some(eds) =>
-          result.append(" ")
-          Isabelle_Syntax.append_list(append_edit, eds, result)
-      }
-    }
-
-    val buf = new StringBuilder(40)
-    buf.append("Isar.edit_document ")
-    Isabelle_Syntax.append_string(old_id, buf)
-    buf.append(" ")
-    Isabelle_Syntax.append_string(new_id, buf)
-    buf.append(" ")
-    Isabelle_Syntax.append_list(append_node_edit, edits, buf)
-    input(buf.toString)
+    input("Isar_Document.edit_document", old_id, new_id, YXML.string_of_body(arg))
   }
 }

--- a/src/Pure/ROOT.ML	Wed Aug 11 00:44:48 2010 +0200
+++ b/src/Pure/ROOT.ML	Wed Aug 11 00:46:07 2010 +0200
@@ -230,7 +230,7 @@
 use "Isar/proof_node.ML";
 use "Isar/toplevel.ML";
 
-(*theory syntax*)
+(*theory documents*)
 use "Thy/present.ML";
 use "Thy/term_style.ML";
 use "Thy/thy_output.ML";
@@ -239,7 +239,6 @@
 use "old_goals.ML";
 use "Isar/outer_syntax.ML";
 use "Thy/thy_info.ML";
-use "Isar/isar_document.ML";
 
 (*theory and proof operations*)
 use "Isar/rule_insts.ML";
@@ -257,6 +256,7 @@
 use "System/session.ML";
 use "System/isar.ML";
 use "System/isabelle_process.ML";
+use "Isar/isar_document.ML";
 
 
 (* miscellaneous tools and packages for Pure Isabelle *)