more robust;
authorwenzelm
Thu, 05 Jan 2023 20:13:04 +0100
changeset 76917 302bdbb3bc05
parent 76916 54947a35ce86
child 76918 19be7d89bf03
more robust;
src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Jan 05 20:07:22 2023 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Jan 05 20:13:04 2023 +0100
@@ -1218,9 +1218,8 @@
           tree <- markup.to_XML(command_range, command.source, elements).iterator
         } yield tree).toList
       }
-      else {
+      else if (node.is_wellformed_text) {
         Text.Range.length(node.source).try_restrict(range) match {
-          case None => Nil
           case Some(node_range) =>
             val markup =
               version.nodes.commands_loading(node_name).headOption match {
@@ -1231,8 +1230,10 @@
                   command_markup(version, command, markup_index, node_range, elements)
               }
             markup.to_XML(node_range, node.source, elements)
+          case None => Nil
         }
       }
+      else Nil
     }
 
     def node_initialized(version: Version, name: Node.Name): Boolean =