more operations;
authorwenzelm
Thu, 05 Jan 2023 20:07:22 +0100
changeset 76916 54947a35ce86
parent 76915 e5f67cfedecd
child 76917 302bdbb3bc05
more operations; more robust;
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)
           }