diff -r 449a989f42cd -r 16f74b7c248a src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Dec 22 18:32:59 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Dec 22 20:15:16 2017 +0100
@@ -821,17 +821,36 @@
 
     def markup_to_XML(
       version: Version,
-      node: Node,
+      node_name: Node.Name,
       range: Text.Range,
       elements: Markup.Elements): XML.Body =
     {
-      (for {
-        command <- node.commands.iterator
-        command_range <- command.range.try_restrict(range).iterator
-        markup =
-          command_markup(version, command, Command.Markup_Index.markup, command_range, elements)
-        tree <- markup.to_XML(command_range, command.source, elements).iterator
-      } yield tree).toList
+      val node = version.nodes(node_name)
+      if (node_name.is_theory) {
+        val markup_index = Command.Markup_Index.markup
+        (for {
+          command <- node.commands.iterator
+          command_range <- command.range.try_restrict(range).iterator
+          markup = command_markup(version, command, markup_index, command_range, elements)
+          tree <- markup.to_XML(command_range, command.source, elements).iterator
+        } yield tree).toList
+      }
+      else {
+        val node_source = Symbol.decode(node.source)  // FIXME treat mixed encode/decode situation
+        Text.Range(0, node_source.length).try_restrict(range) match {
+          case None => Nil
+          case Some(node_range) =>
+            val markup =
+              version.nodes.commands_loading(node_name).headOption match {
+                case None => Markup_Tree.empty
+                case Some(command) =>
+                  val chunk_name = Symbol.Text_Chunk.File(node_name.node)
+                  val markup_index = Command.Markup_Index(false, chunk_name)
+                  command_markup(version, command, markup_index, node_range, elements)
+              }
+            markup.to_XML(node_range, node_source, elements)
+        }
+      }
     }
 
     def node_consolidated(version: Version, name: Node.Name): Boolean =
@@ -910,7 +929,7 @@
           else version.nodes.commands_loading(other_node_name).headOption
 
         def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
-          state.markup_to_XML(version, node, range, elements)
+          state.markup_to_XML(version, node_name, range, elements)
 
 
         /* find command */