# HG changeset patch
# User wenzelm
# Date 1384946694 -3600
# Node ID 842adea880a40ec9faebe1289e3e4cce509dab8e
# Parent  bfeb0ea6c2c0c0657119d3837f39f2fff091016a
refer to thy_load command of auxiliary file;

diff -r bfeb0ea6c2c0 -r 842adea880a4 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Nov 20 12:04:06 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Nov 20 12:24:54 2013 +0100
@@ -253,6 +253,14 @@
     def entries: Iterator[(Node.Name, Node)] =
       graph.entries.map({ case (name, (node, _)) => (name, node) })
 
+    def thy_load_commands(file_name: Node.Name): List[Command] =
+      (for {
+        (_, node) <- entries
+        cmd <- node.thy_load_commands.iterator
+        Exn.Res((name, _)) <- cmd.blobs.iterator
+        if name == file_name
+      } yield cmd).toList
+
     def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names)
     def topological_order: List[Node.Name] = graph.topological_order
   }
diff -r bfeb0ea6c2c0 -r 842adea880a4 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Nov 20 12:04:06 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Nov 20 12:24:54 2013 +0100
@@ -63,11 +63,13 @@
     Swing_Thread.require()
 
     val text_area = view.getTextArea
+    val buffer = view.getBuffer
+
     PIDE.document_view(text_area) match {
       case Some(doc_view) =>
         val node = snapshot.version.nodes(doc_view.model.node_name)
         val caret = snapshot.revert(text_area.getCaretPosition)
-        if (caret < text_area.getBuffer.getLength) {
+        if (caret < buffer.getLength) {
           val caret_commands = node.command_range(caret)
           if (caret_commands.hasNext) {
             val (cmd0, _) = caret_commands.next
@@ -76,7 +78,15 @@
           else None
         }
         else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
-      case None => None
+      case None =>
+        PIDE.document_model(buffer) match {
+          case Some(model) if !model.node_name.is_theory =>
+            snapshot.version.nodes.thy_load_commands(model.node_name) match {
+              case cmd :: _ => Some(cmd)
+              case Nil => None
+            }
+          case _ => None
+        }
     }
   }