support to encode/decode command state;
support to merge full contents of command state;

--- a/src/Pure/General/symbol.scala	Mon Mar 20 17:24:40 2017 +0100
+++ b/src/Pure/General/symbol.scala	Mon Mar 20 20:43:26 2017 +0100
@@ -198,6 +198,25 @@
     case class Id(id: Document_ID.Generic) extends Name
     case class File(name: String) extends Name
 
+    val encode_name: XML.Encode.T[Name] =
+    {
+      import XML.Encode._
+      variant(List(
+        { case Default => (Nil, Nil) },
+        { case Id(a) => (List(long_atom(a)), Nil) },
+        { case File(a) => (List(a), Nil) }))
+    }
+
+    val decode_name: XML.Decode.T[Name] =
+    {
+      import XML.Decode._
+      variant(List(
+        { case (Nil, Nil) => Default },
+        { case (List(a), Nil) => Id(long_atom(a)) },
+        { case (List(a), Nil) => File(a) }))
+    }
+
+
     def apply(text: CharSequence): Text_Chunk =
       new Text_Chunk(Text.Range(0, text.length), Index(text))
   }

--- a/src/Pure/Isar/token.scala	Mon Mar 20 17:24:40 2017 +0100
+++ b/src/Pure/Isar/token.scala	Mon Mar 20 20:43:26 2017 +0100
@@ -218,6 +218,22 @@
 
   def reader(tokens: List[Token], start: Token.Pos): Reader =
     new Token_Reader(tokens, start)
+
+
+  /* XML data representation */
+
+  val encode: XML.Encode.T[Token] = (tok: Token) =>
+  {
+    import XML.Encode._
+    pair(int, string)(tok.kind.id, tok.source)
+  }
+
+  val decode: XML.Decode.T[Token] = (body: XML.Body) =>
+  {
+    import XML.Decode._
+    val (k, s) = pair(int, string)(body)
+    Token(Kind(k), s)
+  }
 }
 
 

--- a/src/Pure/PIDE/command.scala	Mon Mar 20 17:24:40 2017 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Mar 20 20:43:26 2017 +0100
@@ -31,6 +31,15 @@
     val empty = new Results(SortedMap.empty)
     def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
     def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
+
+
+    /* XML data representation */
+
+    val encode: XML.Encode.T[Results] = (results: Results) =>
+    { import XML.Encode._; list(pair(long, tree))(results.rep.toList) }
+
+    val decode: XML.Decode.T[Results] = (body: XML.Body) =>
+    { import XML.Decode._; make(list(pair(long, tree))(body)) }
   }
 
   final class Results private(private val rep: SortedMap[Long, XML.Tree])
@@ -71,9 +80,37 @@
   object Markups
   {
     val empty: Markups = new Markups(Map.empty)
+    def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup))
+    def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _)
 
-    def init(markup: Markup_Tree): Markups =
-      new Markups(Map(Markup_Index.markup -> markup))
+
+    /* XML data representation */
+
+    def encode(source_length: Int): XML.Encode.T[Markups] = (markups: Markups) =>
+    {
+      import XML.Encode._
+
+      val markup_index: T[Markup_Index] = (index: Markup_Index) =>
+        pair(bool, Symbol.Text_Chunk.encode_name)(index.status, index.chunk_name)
+
+      val markup_tree: T[Markup_Tree] =
+        _.to_XML(Text.Range(0, source_length), Symbol.spaces(source_length), Markup.Elements.full)
+
+      list(pair(markup_index, markup_tree))(markups.rep.toList)
+    }
+
+    val decode: XML.Decode.T[Markups] = (body: XML.Body) =>
+    {
+      import XML.Decode._
+
+      val markup_index: T[Markup_Index] = (body: XML.Body) =>
+      {
+        val (status, chunk_name) = pair(bool, Symbol.Text_Chunk.decode_name)(body)
+        Markup_Index(status, chunk_name)
+      }
+
+      (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _)
+    }
   }
 
   final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
@@ -86,6 +123,17 @@
     def add(index: Markup_Index, markup: Text.Markup): Markups =
       new Markups(rep + (index -> (this(index) + markup)))
 
+    def + (entry: (Markup_Index, Markup_Tree)): Markups =
+    {
+      val (index, tree) = entry
+      new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full))))
+    }
+
+    def ++ (other: Markups): Markups =
+      if (this eq other) this
+      else if (rep.isEmpty) other
+      else (this /: other.rep.iterator)(_ + _)
+
     def redirection_iterator: Iterator[Document_ID.Generic] =
       for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
         yield id
@@ -114,12 +162,49 @@
 
   object State
   {
-    def merge_results(states: List[State]): Command.Results =
+    def merge_results(states: List[State]): Results =
       Results.merge(states.map(_.results))
 
+    def merge_markups(states: List[State]): Markups =
+      Markups.merge(states.map(_.markups))
+
     def merge_markup(states: List[State], index: Markup_Index,
         range: Text.Range, elements: Markup.Elements): Markup_Tree =
       Markup_Tree.merge(states.map(_.markup(index)), range, elements)
+
+    def merge(command: Command, states: List[State]): State =
+      State(command, states.flatMap(_.status), merge_results(states), merge_markups(states))
+
+
+    /* XML data representation */
+
+    val encode: XML.Encode.T[State] = (st: State) =>
+    {
+      import XML.Encode._
+
+      val command = st.command
+      val blobs_names = command.blobs_names.map(_.node)
+      val blobs_index = command.blobs_index
+      require(command.blobs_ok)
+
+      pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.encode,
+          pair(list(Markup.encode), pair(Results.encode, Markups.encode(command.source.length)))))))(
+        (command.id, (command.node_name.node, ((blobs_names, blobs_index), (command.span,
+          (st.status, (st.results, st.markups)))))))
+    }
+
+    def decode(node_name: String => Document.Node.Name): XML.Decode.T[State] = (body: XML.Body) =>
+    {
+      import XML.Decode._
+      val (id, (node, ((blobs_names, blobs_index), (span, (status, (results, markups)))))) =
+        pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.decode,
+          pair(list(Markup.decode), pair(Results.decode, Markups.decode))))))(body)
+
+      val blobs_info: Blobs_Info =
+        (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index)
+      val command = Command(id, node_name(node), blobs_info, span)
+      State(command, status, results, markups)
+    }
   }
 
   sealed case class State(
@@ -404,6 +489,9 @@
   def blobs: List[Command.Blob] = blobs_info._1
   def blobs_index: Int = blobs_info._2
 
+  def blobs_ok: Boolean =
+    blobs.forall({ case Exn.Res(_) => true case _ => false })
+
   def blobs_names: List[Document.Node.Name] =
     for (Exn.Res((name, _)) <- blobs) yield name
 

--- a/src/Pure/PIDE/command_span.scala	Mon Mar 20 17:24:40 2017 +0100
+++ b/src/Pure/PIDE/command_span.scala	Mon Mar 20 20:43:26 2017 +0100
@@ -56,4 +56,30 @@
 
   def unparsed(source: String): Span =
     Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
+
+
+  /* XML data representation */
+
+  def encode: XML.Encode.T[Span] = (span: Span) =>
+  {
+    import XML.Encode._
+    val kind: T[Kind] =
+      variant(List(
+        { case Command_Span(a, b) => (List(a), properties(b)) },
+        { case Ignored_Span => (Nil, Nil) },
+        { case Malformed_Span => (Nil, Nil) }))
+    pair(kind, list(Token.encode))((span.kind, span.content))
+  }
+
+  def decode: XML.Decode.T[Span] = (body: XML.Body) =>
+  {
+    import XML.Decode._
+    val kind: T[Kind] =
+      variant(List(
+        { case (List(a), b) => Command_Span(a, properties(b)) },
+        { case (Nil, Nil) => Ignored_Span },
+        { case (Nil, Nil) => Malformed_Span }))
+    val (k, toks) = pair(kind, list(Token.decode))(body)
+    Span(k, toks)
+  }
 }

--- a/src/Pure/PIDE/markup.scala	Mon Mar 20 17:24:40 2017 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Mar 20 20:43:26 2017 +0100
@@ -607,6 +607,22 @@
         case _ => None
       }
   }
+
+
+  /* XML data representation */
+
+  def encode: XML.Encode.T[Markup] = (markup: Markup) =>
+  {
+    import XML.Encode._
+    pair(string, properties)((markup.name, markup.properties))
+  }
+
+  def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
+  {
+    import XML.Decode._
+    val (name, props) = pair(string, properties)(body)
+    Markup(name, props)
+  }
 }