src/Pure/PIDE/command.scala
changeset 65335 7634d33c1a79
parent 64825 e78b62c289bb
child 65341 c82a1620b274
     1.1 --- a/src/Pure/PIDE/command.scala	Mon Mar 20 17:24:40 2017 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Mon Mar 20 20:43:26 2017 +0100
     1.3 @@ -31,6 +31,15 @@
     1.4      val empty = new Results(SortedMap.empty)
     1.5      def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
     1.6      def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
     1.7 +
     1.8 +
     1.9 +    /* XML data representation */
    1.10 +
    1.11 +    val encode: XML.Encode.T[Results] = (results: Results) =>
    1.12 +    { import XML.Encode._; list(pair(long, tree))(results.rep.toList) }
    1.13 +
    1.14 +    val decode: XML.Decode.T[Results] = (body: XML.Body) =>
    1.15 +    { import XML.Decode._; make(list(pair(long, tree))(body)) }
    1.16    }
    1.17  
    1.18    final class Results private(private val rep: SortedMap[Long, XML.Tree])
    1.19 @@ -71,9 +80,37 @@
    1.20    object Markups
    1.21    {
    1.22      val empty: Markups = new Markups(Map.empty)
    1.23 +    def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup))
    1.24 +    def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _)
    1.25  
    1.26 -    def init(markup: Markup_Tree): Markups =
    1.27 -      new Markups(Map(Markup_Index.markup -> markup))
    1.28 +
    1.29 +    /* XML data representation */
    1.30 +
    1.31 +    def encode(source_length: Int): XML.Encode.T[Markups] = (markups: Markups) =>
    1.32 +    {
    1.33 +      import XML.Encode._
    1.34 +
    1.35 +      val markup_index: T[Markup_Index] = (index: Markup_Index) =>
    1.36 +        pair(bool, Symbol.Text_Chunk.encode_name)(index.status, index.chunk_name)
    1.37 +
    1.38 +      val markup_tree: T[Markup_Tree] =
    1.39 +        _.to_XML(Text.Range(0, source_length), Symbol.spaces(source_length), Markup.Elements.full)
    1.40 +
    1.41 +      list(pair(markup_index, markup_tree))(markups.rep.toList)
    1.42 +    }
    1.43 +
    1.44 +    val decode: XML.Decode.T[Markups] = (body: XML.Body) =>
    1.45 +    {
    1.46 +      import XML.Decode._
    1.47 +
    1.48 +      val markup_index: T[Markup_Index] = (body: XML.Body) =>
    1.49 +      {
    1.50 +        val (status, chunk_name) = pair(bool, Symbol.Text_Chunk.decode_name)(body)
    1.51 +        Markup_Index(status, chunk_name)
    1.52 +      }
    1.53 +
    1.54 +      (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _)
    1.55 +    }
    1.56    }
    1.57  
    1.58    final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
    1.59 @@ -86,6 +123,17 @@
    1.60      def add(index: Markup_Index, markup: Text.Markup): Markups =
    1.61        new Markups(rep + (index -> (this(index) + markup)))
    1.62  
    1.63 +    def + (entry: (Markup_Index, Markup_Tree)): Markups =
    1.64 +    {
    1.65 +      val (index, tree) = entry
    1.66 +      new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full))))
    1.67 +    }
    1.68 +
    1.69 +    def ++ (other: Markups): Markups =
    1.70 +      if (this eq other) this
    1.71 +      else if (rep.isEmpty) other
    1.72 +      else (this /: other.rep.iterator)(_ + _)
    1.73 +
    1.74      def redirection_iterator: Iterator[Document_ID.Generic] =
    1.75        for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
    1.76          yield id
    1.77 @@ -114,12 +162,49 @@
    1.78  
    1.79    object State
    1.80    {
    1.81 -    def merge_results(states: List[State]): Command.Results =
    1.82 +    def merge_results(states: List[State]): Results =
    1.83        Results.merge(states.map(_.results))
    1.84  
    1.85 +    def merge_markups(states: List[State]): Markups =
    1.86 +      Markups.merge(states.map(_.markups))
    1.87 +
    1.88      def merge_markup(states: List[State], index: Markup_Index,
    1.89          range: Text.Range, elements: Markup.Elements): Markup_Tree =
    1.90        Markup_Tree.merge(states.map(_.markup(index)), range, elements)
    1.91 +
    1.92 +    def merge(command: Command, states: List[State]): State =
    1.93 +      State(command, states.flatMap(_.status), merge_results(states), merge_markups(states))
    1.94 +
    1.95 +
    1.96 +    /* XML data representation */
    1.97 +
    1.98 +    val encode: XML.Encode.T[State] = (st: State) =>
    1.99 +    {
   1.100 +      import XML.Encode._
   1.101 +
   1.102 +      val command = st.command
   1.103 +      val blobs_names = command.blobs_names.map(_.node)
   1.104 +      val blobs_index = command.blobs_index
   1.105 +      require(command.blobs_ok)
   1.106 +
   1.107 +      pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.encode,
   1.108 +          pair(list(Markup.encode), pair(Results.encode, Markups.encode(command.source.length)))))))(
   1.109 +        (command.id, (command.node_name.node, ((blobs_names, blobs_index), (command.span,
   1.110 +          (st.status, (st.results, st.markups)))))))
   1.111 +    }
   1.112 +
   1.113 +    def decode(node_name: String => Document.Node.Name): XML.Decode.T[State] = (body: XML.Body) =>
   1.114 +    {
   1.115 +      import XML.Decode._
   1.116 +      val (id, (node, ((blobs_names, blobs_index), (span, (status, (results, markups)))))) =
   1.117 +        pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.decode,
   1.118 +          pair(list(Markup.decode), pair(Results.decode, Markups.decode))))))(body)
   1.119 +
   1.120 +      val blobs_info: Blobs_Info =
   1.121 +        (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index)
   1.122 +      val command = Command(id, node_name(node), blobs_info, span)
   1.123 +      State(command, status, results, markups)
   1.124 +    }
   1.125    }
   1.126  
   1.127    sealed case class State(
   1.128 @@ -404,6 +489,9 @@
   1.129    def blobs: List[Command.Blob] = blobs_info._1
   1.130    def blobs_index: Int = blobs_info._2
   1.131  
   1.132 +  def blobs_ok: Boolean =
   1.133 +    blobs.forall({ case Exn.Res(_) => true case _ => false })
   1.134 +
   1.135    def blobs_names: List[Document.Node.Name] =
   1.136      for (Exn.Res((name, _)) <- blobs) yield name
   1.137