# HG changeset patch # User wenzelm # Date 1606491631 -3600 # Node ID 0017eb17ac1c459452e2d6ef32fe28350915f004 # Parent bc82fc6054243bcc611f1bf4471c2f0aa07ef727 unused (see 7634d33c1a79); diff -r bc82fc605424 -r 0017eb17ac1c src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri Nov 27 14:25:39 2020 +0100 +++ b/src/Pure/General/symbol.scala Fri Nov 27 16:40:31 2020 +0100 @@ -214,24 +214,6 @@ 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 bc82fc605424 -r 0017eb17ac1c src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Fri Nov 27 14:25:39 2020 +0100 +++ b/src/Pure/Isar/token.scala Fri Nov 27 16:40:31 2020 +0100 @@ -256,22 +256,6 @@ 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 bc82fc605424 -r 0017eb17ac1c src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri Nov 27 14:25:39 2020 +0100 +++ b/src/Pure/PIDE/command.scala Fri Nov 27 16:40:31 2020 +0100 @@ -31,15 +31,6 @@ val empty: Results = 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]) @@ -115,35 +106,6 @@ 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)(_ ++ _) - - - /* 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]) @@ -221,37 +183,6 @@ def merge(command: Command, states: List[State]): State = State(command, states.flatMap(_.status), merge_results(states), merge_exports(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, Exports.empty, markups) - } } sealed case class State( diff -r bc82fc605424 -r 0017eb17ac1c src/Pure/PIDE/command_span.scala --- a/src/Pure/PIDE/command_span.scala Fri Nov 27 14:25:39 2020 +0100 +++ b/src/Pure/PIDE/command_span.scala Fri Nov 27 16:40:31 2020 +0100 @@ -119,30 +119,4 @@ val kind = if (theory) Theory_Span else Malformed_Span Span(kind, 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) - } }