support to encode/decode command state;
authorwenzelm
Mon Mar 20 20:43:26 2017 +0100 (2017-03-20)
changeset 653357634d33c1a79
parent 65334 264a3904ab5a
child 65336 8e5274fc0093
support to encode/decode command state;
support to merge full contents of command state;
src/Pure/General/symbol.scala
src/Pure/Isar/token.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/command_span.scala
src/Pure/PIDE/markup.scala
     1.1 --- a/src/Pure/General/symbol.scala	Mon Mar 20 17:24:40 2017 +0100
     1.2 +++ b/src/Pure/General/symbol.scala	Mon Mar 20 20:43:26 2017 +0100
     1.3 @@ -198,6 +198,25 @@
     1.4      case class Id(id: Document_ID.Generic) extends Name
     1.5      case class File(name: String) extends Name
     1.6  
     1.7 +    val encode_name: XML.Encode.T[Name] =
     1.8 +    {
     1.9 +      import XML.Encode._
    1.10 +      variant(List(
    1.11 +        { case Default => (Nil, Nil) },
    1.12 +        { case Id(a) => (List(long_atom(a)), Nil) },
    1.13 +        { case File(a) => (List(a), Nil) }))
    1.14 +    }
    1.15 +
    1.16 +    val decode_name: XML.Decode.T[Name] =
    1.17 +    {
    1.18 +      import XML.Decode._
    1.19 +      variant(List(
    1.20 +        { case (Nil, Nil) => Default },
    1.21 +        { case (List(a), Nil) => Id(long_atom(a)) },
    1.22 +        { case (List(a), Nil) => File(a) }))
    1.23 +    }
    1.24 +
    1.25 +
    1.26      def apply(text: CharSequence): Text_Chunk =
    1.27        new Text_Chunk(Text.Range(0, text.length), Index(text))
    1.28    }
     2.1 --- a/src/Pure/Isar/token.scala	Mon Mar 20 17:24:40 2017 +0100
     2.2 +++ b/src/Pure/Isar/token.scala	Mon Mar 20 20:43:26 2017 +0100
     2.3 @@ -218,6 +218,22 @@
     2.4  
     2.5    def reader(tokens: List[Token], start: Token.Pos): Reader =
     2.6      new Token_Reader(tokens, start)
     2.7 +
     2.8 +
     2.9 +  /* XML data representation */
    2.10 +
    2.11 +  val encode: XML.Encode.T[Token] = (tok: Token) =>
    2.12 +  {
    2.13 +    import XML.Encode._
    2.14 +    pair(int, string)(tok.kind.id, tok.source)
    2.15 +  }
    2.16 +
    2.17 +  val decode: XML.Decode.T[Token] = (body: XML.Body) =>
    2.18 +  {
    2.19 +    import XML.Decode._
    2.20 +    val (k, s) = pair(int, string)(body)
    2.21 +    Token(Kind(k), s)
    2.22 +  }
    2.23  }
    2.24  
    2.25  
     3.1 --- a/src/Pure/PIDE/command.scala	Mon Mar 20 17:24:40 2017 +0100
     3.2 +++ b/src/Pure/PIDE/command.scala	Mon Mar 20 20:43:26 2017 +0100
     3.3 @@ -31,6 +31,15 @@
     3.4      val empty = new Results(SortedMap.empty)
     3.5      def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
     3.6      def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
     3.7 +
     3.8 +
     3.9 +    /* XML data representation */
    3.10 +
    3.11 +    val encode: XML.Encode.T[Results] = (results: Results) =>
    3.12 +    { import XML.Encode._; list(pair(long, tree))(results.rep.toList) }
    3.13 +
    3.14 +    val decode: XML.Decode.T[Results] = (body: XML.Body) =>
    3.15 +    { import XML.Decode._; make(list(pair(long, tree))(body)) }
    3.16    }
    3.17  
    3.18    final class Results private(private val rep: SortedMap[Long, XML.Tree])
    3.19 @@ -71,9 +80,37 @@
    3.20    object Markups
    3.21    {
    3.22      val empty: Markups = new Markups(Map.empty)
    3.23 +    def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup))
    3.24 +    def merge(args: TraversableOnce[Markups]): Markups = (empty /: args)(_ ++ _)
    3.25  
    3.26 -    def init(markup: Markup_Tree): Markups =
    3.27 -      new Markups(Map(Markup_Index.markup -> markup))
    3.28 +
    3.29 +    /* XML data representation */
    3.30 +
    3.31 +    def encode(source_length: Int): XML.Encode.T[Markups] = (markups: Markups) =>
    3.32 +    {
    3.33 +      import XML.Encode._
    3.34 +
    3.35 +      val markup_index: T[Markup_Index] = (index: Markup_Index) =>
    3.36 +        pair(bool, Symbol.Text_Chunk.encode_name)(index.status, index.chunk_name)
    3.37 +
    3.38 +      val markup_tree: T[Markup_Tree] =
    3.39 +        _.to_XML(Text.Range(0, source_length), Symbol.spaces(source_length), Markup.Elements.full)
    3.40 +
    3.41 +      list(pair(markup_index, markup_tree))(markups.rep.toList)
    3.42 +    }
    3.43 +
    3.44 +    val decode: XML.Decode.T[Markups] = (body: XML.Body) =>
    3.45 +    {
    3.46 +      import XML.Decode._
    3.47 +
    3.48 +      val markup_index: T[Markup_Index] = (body: XML.Body) =>
    3.49 +      {
    3.50 +        val (status, chunk_name) = pair(bool, Symbol.Text_Chunk.decode_name)(body)
    3.51 +        Markup_Index(status, chunk_name)
    3.52 +      }
    3.53 +
    3.54 +      (Markups.empty /: list(pair(markup_index, Markup_Tree.from_XML(_)))(body))(_ + _)
    3.55 +    }
    3.56    }
    3.57  
    3.58    final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
    3.59 @@ -86,6 +123,17 @@
    3.60      def add(index: Markup_Index, markup: Text.Markup): Markups =
    3.61        new Markups(rep + (index -> (this(index) + markup)))
    3.62  
    3.63 +    def + (entry: (Markup_Index, Markup_Tree)): Markups =
    3.64 +    {
    3.65 +      val (index, tree) = entry
    3.66 +      new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full))))
    3.67 +    }
    3.68 +
    3.69 +    def ++ (other: Markups): Markups =
    3.70 +      if (this eq other) this
    3.71 +      else if (rep.isEmpty) other
    3.72 +      else (this /: other.rep.iterator)(_ + _)
    3.73 +
    3.74      def redirection_iterator: Iterator[Document_ID.Generic] =
    3.75        for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
    3.76          yield id
    3.77 @@ -114,12 +162,49 @@
    3.78  
    3.79    object State
    3.80    {
    3.81 -    def merge_results(states: List[State]): Command.Results =
    3.82 +    def merge_results(states: List[State]): Results =
    3.83        Results.merge(states.map(_.results))
    3.84  
    3.85 +    def merge_markups(states: List[State]): Markups =
    3.86 +      Markups.merge(states.map(_.markups))
    3.87 +
    3.88      def merge_markup(states: List[State], index: Markup_Index,
    3.89          range: Text.Range, elements: Markup.Elements): Markup_Tree =
    3.90        Markup_Tree.merge(states.map(_.markup(index)), range, elements)
    3.91 +
    3.92 +    def merge(command: Command, states: List[State]): State =
    3.93 +      State(command, states.flatMap(_.status), merge_results(states), merge_markups(states))
    3.94 +
    3.95 +
    3.96 +    /* XML data representation */
    3.97 +
    3.98 +    val encode: XML.Encode.T[State] = (st: State) =>
    3.99 +    {
   3.100 +      import XML.Encode._
   3.101 +
   3.102 +      val command = st.command
   3.103 +      val blobs_names = command.blobs_names.map(_.node)
   3.104 +      val blobs_index = command.blobs_index
   3.105 +      require(command.blobs_ok)
   3.106 +
   3.107 +      pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.encode,
   3.108 +          pair(list(Markup.encode), pair(Results.encode, Markups.encode(command.source.length)))))))(
   3.109 +        (command.id, (command.node_name.node, ((blobs_names, blobs_index), (command.span,
   3.110 +          (st.status, (st.results, st.markups)))))))
   3.111 +    }
   3.112 +
   3.113 +    def decode(node_name: String => Document.Node.Name): XML.Decode.T[State] = (body: XML.Body) =>
   3.114 +    {
   3.115 +      import XML.Decode._
   3.116 +      val (id, (node, ((blobs_names, blobs_index), (span, (status, (results, markups)))))) =
   3.117 +        pair(long, pair(string, pair(pair(list(string), int), pair(Command_Span.decode,
   3.118 +          pair(list(Markup.decode), pair(Results.decode, Markups.decode))))))(body)
   3.119 +
   3.120 +      val blobs_info: Blobs_Info =
   3.121 +        (blobs_names.map(name => Exn.Res((node_name(name), None)): Blob), blobs_index)
   3.122 +      val command = Command(id, node_name(node), blobs_info, span)
   3.123 +      State(command, status, results, markups)
   3.124 +    }
   3.125    }
   3.126  
   3.127    sealed case class State(
   3.128 @@ -404,6 +489,9 @@
   3.129    def blobs: List[Command.Blob] = blobs_info._1
   3.130    def blobs_index: Int = blobs_info._2
   3.131  
   3.132 +  def blobs_ok: Boolean =
   3.133 +    blobs.forall({ case Exn.Res(_) => true case _ => false })
   3.134 +
   3.135    def blobs_names: List[Document.Node.Name] =
   3.136      for (Exn.Res((name, _)) <- blobs) yield name
   3.137  
     4.1 --- a/src/Pure/PIDE/command_span.scala	Mon Mar 20 17:24:40 2017 +0100
     4.2 +++ b/src/Pure/PIDE/command_span.scala	Mon Mar 20 20:43:26 2017 +0100
     4.3 @@ -56,4 +56,30 @@
     4.4  
     4.5    def unparsed(source: String): Span =
     4.6      Span(Malformed_Span, List(Token(Token.Kind.UNPARSED, source)))
     4.7 +
     4.8 +
     4.9 +  /* XML data representation */
    4.10 +
    4.11 +  def encode: XML.Encode.T[Span] = (span: Span) =>
    4.12 +  {
    4.13 +    import XML.Encode._
    4.14 +    val kind: T[Kind] =
    4.15 +      variant(List(
    4.16 +        { case Command_Span(a, b) => (List(a), properties(b)) },
    4.17 +        { case Ignored_Span => (Nil, Nil) },
    4.18 +        { case Malformed_Span => (Nil, Nil) }))
    4.19 +    pair(kind, list(Token.encode))((span.kind, span.content))
    4.20 +  }
    4.21 +
    4.22 +  def decode: XML.Decode.T[Span] = (body: XML.Body) =>
    4.23 +  {
    4.24 +    import XML.Decode._
    4.25 +    val kind: T[Kind] =
    4.26 +      variant(List(
    4.27 +        { case (List(a), b) => Command_Span(a, properties(b)) },
    4.28 +        { case (Nil, Nil) => Ignored_Span },
    4.29 +        { case (Nil, Nil) => Malformed_Span }))
    4.30 +    val (k, toks) = pair(kind, list(Token.decode))(body)
    4.31 +    Span(k, toks)
    4.32 +  }
    4.33  }
     5.1 --- a/src/Pure/PIDE/markup.scala	Mon Mar 20 17:24:40 2017 +0100
     5.2 +++ b/src/Pure/PIDE/markup.scala	Mon Mar 20 20:43:26 2017 +0100
     5.3 @@ -607,6 +607,22 @@
     5.4          case _ => None
     5.5        }
     5.6    }
     5.7 +
     5.8 +
     5.9 +  /* XML data representation */
    5.10 +
    5.11 +  def encode: XML.Encode.T[Markup] = (markup: Markup) =>
    5.12 +  {
    5.13 +    import XML.Encode._
    5.14 +    pair(string, properties)((markup.name, markup.properties))
    5.15 +  }
    5.16 +
    5.17 +  def decode: XML.Decode.T[Markup] = (body: XML.Body) =>
    5.18 +  {
    5.19 +    import XML.Decode._
    5.20 +    val (name, props) = pair(string, properties)(body)
    5.21 +    Markup(name, props)
    5.22 +  }
    5.23  }
    5.24  
    5.25