# HG changeset patch
# User wenzelm
# Date 1440503184 -7200
# Node ID 46df28442a800da0f57b7788ec258ce1b052dcca
# Parent  1c4ae64636bbb2252a929a4d54ed5e1216c43807
clarified undefined_blobs: already loaded theories are suppressed;
enabled jedit_auto_resolve (again): e.g. relevant for debugging when following links through source files;

diff -r 1c4ae64636bb -r 46df28442a80 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 25 10:41:12 2015 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 25 13:46:24 2015 +0200
@@ -347,9 +347,10 @@
         if name == file_name
       } yield cmd).toList
 
-    def undefined_blobs: List[Node.Name] =
+    def undefined_blobs(pred: Node.Name => Boolean): List[Node.Name] =
       (for {
-        (_, node) <- iterator
+        (node_name, node) <- iterator
+        if pred(node_name)
         cmd <- node.load_commands.iterator
         name <- cmd.blobs_undefined.iterator
       } yield name).toList
diff -r 1c4ae64636bb -r 46df28442a80 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue Aug 25 10:41:12 2015 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Aug 25 13:46:24 2015 +0200
@@ -9,7 +9,7 @@
 public option jedit_auto_load : bool = false
   -- "load all required files automatically to resolve theory imports"
 
-public option jedit_auto_resolve : bool = false
+public option jedit_auto_resolve : bool = true
   -- "automatically resolve auxiliary files within the editor"
 
 public option jedit_reset_font_size : int = 18
diff -r 1c4ae64636bb -r 46df28442a80 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Aug 25 10:41:12 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Aug 25 13:46:24 2015 +0200
@@ -111,6 +111,9 @@
 
   /* theory text edits */
 
+  def undefined_blobs(nodes: Document.Nodes): List[Document.Node.Name] =
+    nodes.undefined_blobs(node => !loaded_theories(node.theory))
+
   override def commit(change: Session.Change)
   {
     if (change.syntax_changed.nonEmpty)
@@ -123,7 +126,7 @@
         } model.syntax_changed()
       }
     if (change.deps_changed ||
-        PIDE.options.bool("jedit_auto_resolve") && change.version.nodes.undefined_blobs.nonEmpty)
+        PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version.nodes).nonEmpty)
       PIDE.deps_changed()
   }
 }
diff -r 1c4ae64636bb -r 46df28442a80 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 25 10:41:12 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 25 13:46:24 2015 +0200
@@ -222,7 +222,7 @@
             val aux_files =
               if (PIDE.options.bool("jedit_auto_resolve")) {
                 PIDE.editor.stable_tip_version() match {
-                  case Some(version) => version.nodes.undefined_blobs.map(_.node)
+                  case Some(version) => PIDE.resources.undefined_blobs(version.nodes).map(_.node)
                   case None => Nil
                 }
               }