diff -r e5f67cfedecd -r 54947a35ce86 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Thu Jan 05 19:41:12 2023 +0100 +++ b/src/Pure/PIDE/document.scala Thu Jan 05 20:07:22 2023 +0100 @@ -42,7 +42,13 @@ /* document blobs: auxiliary files */ object Blobs { - sealed case class Item(bytes: Bytes, source: String, chunk: Symbol.Text_Chunk, changed: Boolean) { + sealed case class Item( + bytes: Bytes, + source: String, + chunk: Symbol.Text_Chunk, + changed: Boolean + ) { + def is_wellformed_text: Boolean = bytes.wellformed_text.nonEmpty def unchanged: Item = copy(changed = false) } @@ -337,6 +343,12 @@ def command_start(cmd: Command): Option[Text.Offset] = Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2) + lazy val is_wellformed_text: Boolean = + get_blob match { + case Some(blob) => blob.is_wellformed_text + case None => true + } + lazy val source: String = get_blob match { case Some(blob) => blob.source @@ -644,9 +656,13 @@ snippet_command match { case None => Nil case Some(command) => - for (Exn.Res(blob) <- command.blobs) + for { + Exn.Res(blob) <- command.blobs + blob_node = get_node(blob.name) + if blob_node.is_wellformed_text + } yield { - val text = get_node(blob.name).source + 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) }