# HG changeset patch
# User wenzelm
# Date 1731247864 -3600
# Node ID 92fb366f708a57cebd38cad3d31276e971cb7fe5
# Parent  41374ed08c9f97bb2b5dfefb89116093af8cf289
obsolete;

diff -r 41374ed08c9f -r 92fb366f708a src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sun Nov 10 15:10:51 2024 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Nov 10 15:11:04 2024 +0100
@@ -386,15 +386,6 @@
     new Command(id, node_name, blobs_info, span1, source1, results, markups)
   }
 
-  def rich_text(
-    body: XML.Body = Nil,
-    id: Document_ID.Command = Document_ID.none,
-    results: Results = Results.empty
-  ): Command = {
-    unparsed(XML.content(body), id = id, results = results,
-      markups = Markups.init(Markup_Tree.from_XML(body)))
-  }
-
 
   /* edits and perspective */