diff -r 9ce0aa145d21 -r cca0b48ca891 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Jan 06 14:58:13 2023 +0100 +++ b/src/Pure/PIDE/document.scala Fri Jan 06 14:59:59 2023 +0100 @@ -650,25 +650,6 @@ elements: Markup.Elements = Markup.Elements.full): XML.Body = state.xml_markup(version, node_name, range = range, elements = elements) - def xml_markup_blobs( - elements: Markup.Elements = Markup.Elements.full - ) : List[(Command.Blob, XML.Body)] = { - snippet_command match { - case None => Nil - case Some(command) => - for { - Exn.Res(blob) <- command.blobs - blob_node = get_node(blob.name) - if blob_node.source_wellformed - } - yield { - val text = blob_node.source - val markup = command.init_markups(Command.Markup_Index.blob(blob)) - blob -> markup.to_XML(Text.Range.length(text), text, elements) - } - } - } - /* messages */