# HG changeset patch # User wenzelm # Date 1490039006 -3600 # Node ID 7634d33c1a79833a15a86249042f8b5aa0eca95f # Parent 264a3904ab5a87dcadfa4a721460c623db8b6f52 support to encode/decode command state; support to merge full contents of command state; diff -r 264a3904ab5a -r 7634d33c1a79 src/Pure/General/symbol.scala --- 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)) } diff -r 264a3904ab5a -r 7634d33c1a79 src/Pure/Isar/token.scala --- 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) + } } diff -r 264a3904ab5a -r 7634d33c1a79 src/Pure/PIDE/command.scala --- 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 diff -r 264a3904ab5a -r 7634d33c1a79 src/Pure/PIDE/command_span.scala --- 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) + } } diff -r 264a3904ab5a -r 7634d33c1a79 src/Pure/PIDE/markup.scala --- 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) + } }