# HG changeset patch
# User wenzelm
# Date 1672945984 -3600
# Node ID 302bdbb3bc05ed2652db56d94d6f460194c33bdb
# Parent  54947a35ce86d0d86379b17aa1d3708494cfff2c
more robust;

diff -r 54947a35ce86 -r 302bdbb3bc05 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 =