diff -r 6c360a6ade0e -r c9bb76303348 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Nov 17 16:02:06 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Nov 17 17:22:55 2013 +0100
@@ -148,6 +148,9 @@
 
     final class Commands private(val commands: Linear_Set[Command])
     {
+      lazy val thy_load_commands: List[Command] =
+        commands.iterator.filter(_.thy_load.isDefined).toList
+
       private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
       {
         val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
@@ -197,6 +200,7 @@
       perspective.overlays == other_perspective.overlays
 
     def commands: Linear_Set[Command] = _commands.commands
+    def thy_load_commands: List[Command] = _commands.thy_load_commands
 
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this