unused (see 7634d33c1a79);

--- 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))
   }

--- 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)
-  }
 }
 
 

--- 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(

--- 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)
-  }
 }