--- 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 */