diff -r e0f20a44ff9d -r 9c53198dbb1c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Feb 11 17:44:29 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Tue Feb 11 21:58:31 2014 +0100
@@ -361,6 +361,7 @@
 
     val node_name: Node.Name
     val node: Node
+    val thy_load_commands: List[Command]
     def eq_content(other: Snapshot): Boolean
     def cumulate_markup[A](
       range: Text.Range,
@@ -608,6 +609,10 @@
         val node_name = name
         val node = version.nodes(name)
 
+        val thy_load_commands: List[Command] =
+          if (node_name.is_theory) Nil
+          else version.nodes.thy_load_commands(node_name)
+
         def eq_content(other: Snapshot): Boolean =
           !is_outdated && !other.is_outdated &&
             node.commands.size == other.node.commands.size &&
@@ -621,15 +626,30 @@
           result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
         {
           val former_range = revert(range)
-          (for {
-            (command, command_start) <- node.command_range(former_range)
-            st = state.command_state(version, command)
-            res = result(st)
-            Text.Info(r0, a) <- st.markup.cumulate[A](
-              (former_range - command_start).restrict(command.range), info, elements,
-              { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
-            ).iterator
-          } yield Text.Info(convert(r0 + command_start), a)).toList
+          thy_load_commands match {
+            case thy_load_command :: _ =>
+              val file_name = node_name.node
+              (for {
+                chunk <- thy_load_command.chunks.get(file_name).iterator
+                st = state.command_state(version, thy_load_command)
+                res = result(st)
+                Text.Info(r0, a) <- st.get_markup(file_name).cumulate[A](
+                  former_range.restrict(chunk.range), info, elements,
+                  { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
+                ).iterator
+              } yield Text.Info(convert(r0), a)).toList
+
+            case _ =>
+              (for {
+                (command, command_start) <- node.command_range(former_range)
+                st = state.command_state(version, command)
+                res = result(st)
+                Text.Info(r0, a) <- st.markup.cumulate[A](
+                  (former_range - command_start).restrict(command.range), info, elements,
+                  { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }
+                ).iterator
+              } yield Text.Info(convert(r0 + command_start), a)).toList
+          }
         }
 
         def select_markup[A](range: Text.Range, elements: Option[Set[String]],