# HG changeset patch
# User wenzelm
# Date 1314992907 -7200
# Node ID 383c9d758a56247577ca129169bb7ad9bcc4ffd0
# Parent  90bab3febb6caf2e019c4c8f97484e8e38439f6d
raw message function "assign_execs" avoids full overhead of decoding and caching message body;

diff -r 90bab3febb6c -r 383c9d758a56 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Sep 02 21:06:05 2011 +0200
+++ b/src/Pure/General/markup.ML	Fri Sep 02 21:48:27 2011 +0200
@@ -107,8 +107,6 @@
   val joinedN: string val joined: T
   val failedN: string val failed: T
   val finishedN: string val finished: T
-  val versionN: string
-  val assignN: string val assign: int -> T
   val serialN: string
   val legacyN: string val legacy: T
   val promptN: string val prompt: T
@@ -117,6 +115,7 @@
   val no_reportN: string val no_report: T
   val badN: string val bad: T
   val functionN: string
+  val assign_execs: Properties.T
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
   val no_output: Output.output * Output.output
@@ -349,12 +348,6 @@
 val (finishedN, finished) = markup_elem "finished";
 
 
-(* interactive documents *)
-
-val versionN = "version";
-val (assignN, assign) = markup_int "assign" versionN;
-
-
 (* messages *)
 
 val serialN = "serial";
@@ -373,6 +366,8 @@
 
 val functionN = "function"
 
+val assign_execs = [(functionN, "assign_execs")];
+
 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
 
diff -r 90bab3febb6c -r 383c9d758a56 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Fri Sep 02 21:06:05 2011 +0200
+++ b/src/Pure/General/markup.scala	Fri Sep 02 21:48:27 2011 +0200
@@ -273,6 +273,8 @@
   val FUNCTION = "function"
   val Function = new Properties.String(FUNCTION)
 
+  val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
+
   val INVOKE_SCALA = "invoke_scala"
   object Invoke_Scala
   {
diff -r 90bab3febb6c -r 383c9d758a56 src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Fri Sep 02 21:06:05 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Fri Sep 02 21:48:27 2011 +0200
@@ -56,11 +56,11 @@
         val (assignment, state1) = Document.update old_id new_id edits state;
         val _ = Future.join_tasks running;
         val _ =
-          Output.status (Markup.markup (Markup.assign new_id)
-            (assignment |>
+          Output.raw_message Markup.assign_execs
+            ((new_id, assignment) |>
               let open XML.Encode
-              in pair (list (pair int (option int))) (list (pair string (option int))) end
-              |> YXML.string_of_body));
+              in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
+              |> YXML.string_of_body);
         val state2 = Document.execute new_id state1;
       in state2 end));
 
diff -r 90bab3febb6c -r 383c9d758a56 src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Fri Sep 02 21:06:05 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 02 21:48:27 2011 +0200
@@ -13,19 +13,16 @@
 
   object Assign
   {
-    def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] =
-      msg match {
-        case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) =>
-          try {
-            import XML.Decode._
-            val a = pair(list(pair(long, option(long))), list(pair(string, option(long))))(body)
-            Some(id, a)
-          }
-          catch {
-            case _: XML.XML_Atom => None
-            case _: XML.XML_Body => None
-          }
-        case _ => None
+    def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
+      try {
+        import XML.Decode._
+        val body = YXML.parse_body(text)
+        Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
+      }
+      catch {
+        case ERROR(_) => None
+        case _: XML.XML_Atom => None
+        case _: XML.XML_Body => None
       }
   }
 
diff -r 90bab3febb6c -r 383c9d758a56 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Sep 02 21:06:05 2011 +0200
+++ b/src/Pure/System/session.scala	Fri Sep 02 21:48:27 2011 +0200
@@ -288,6 +288,13 @@
           catch {
             case _: Document.State.Fail => bad_result(result)
           }
+        case Markup.Assign_Execs if result.is_raw =>
+          XML.content(result.body).mkString match {
+            case Isar_Document.Assign(id, assign) =>
+              try { handle_assign(id, assign) }
+              catch { case _: Document.State.Fail => bad_result(result) }
+            case _ => bad_result(result)
+          }
         case Markup.Invoke_Scala(name, id) if result.is_raw =>
           Future.fork {
             val arg = XML.content(result.body).mkString
@@ -311,9 +318,6 @@
           else if (result.is_stdout) { }
           else if (result.is_status) {
             result.body match {
-              case List(Isar_Document.Assign(id, assign)) =>
-                try { handle_assign(id, assign) }
-                catch { case _: Document.State.Fail => bad_result(result) }
               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
               case List(Keyword.Keyword_Decl(name)) => syntax += name
               case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)