# HG changeset patch
# User wenzelm
# Date 1439380431 -7200
# Node ID a6e2a667b0a84033683a95d0ac0e0d0e8dfae628
# Parent  2986137093c6571af30635374ea1a69b880bb8e5
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;

diff -r 2986137093c6 -r a6e2a667b0a8 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Aug 12 03:07:01 2015 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Aug 12 13:53:51 2015 +0200
@@ -413,6 +413,9 @@
   def blobs_names: List[Document.Node.Name] =
     for (Exn.Res((name, _)) <- blobs) yield name
 
+  def blobs_undefined: List[Document.Node.Name] =
+    for (Exn.Res((name, None)) <- blobs) yield name
+
   def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] =
     for (Exn.Res((name, Some((digest, _)))) <- blobs) yield (name, digest)
 
diff -r 2986137093c6 -r a6e2a667b0a8 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Aug 12 03:07:01 2015 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Aug 12 13:53:51 2015 +0200
@@ -347,6 +347,13 @@
         if name == file_name
       } yield cmd).toList
 
+    def undefined_blobs: List[Node.Name] =
+      (for {
+        (_, node) <- iterator
+        cmd <- node.load_commands.iterator
+        name <- cmd.blobs_undefined.iterator
+      } yield name).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 2986137093c6 -r a6e2a667b0a8 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Aug 12 03:07:01 2015 +0200
+++ b/src/Tools/jEdit/etc/options	Wed Aug 12 13:53:51 2015 +0200
@@ -9,6 +9,9 @@
 public option jedit_auto_load : bool = false
   -- "load all required files automatically to resolve theory imports"
 
+public option jedit_auto_resolve : bool = true
+  -- "automatically resolve auxiliary files within the editor"
+
 public option jedit_reset_font_size : int = 18
   -- "reset main text font size"
 
diff -r 2986137093c6 -r a6e2a667b0a8 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Wed Aug 12 03:07:01 2015 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Aug 12 13:53:51 2015 +0200
@@ -122,6 +122,8 @@
           if changed(model.node_name)
         } model.syntax_changed()
       }
-    if (change.deps_changed && PIDE.options.bool("jedit_auto_load")) PIDE.deps_changed()
+    if (PIDE.options.bool("jedit_auto_load") && change.deps_changed ||
+        PIDE.options.bool("jedit_auto_resolve") && change.version.nodes.undefined_blobs.nonEmpty)
+      PIDE.deps_changed()
   }
 }
diff -r 2986137093c6 -r a6e2a667b0a8 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 12 03:07:01 2015 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 12 13:53:51 2015 +0200
@@ -217,8 +217,19 @@
               } yield (model.node_name, Position.none)
 
             val thy_info = new Thy_Info(PIDE.resources)
-            val files = thy_info.dependencies("", thys).deps.map(_.name.node).
-              filter(file => !loaded_buffer(file) && PIDE.resources.check_file(file))
+            val thy_files = thy_info.dependencies("", thys).deps.map(_.name.node)
+
+            val aux_files =
+              if (PIDE.options.bool("jedit_auto_resolve")) {
+                val snapshot = PIDE.snapshot(view)
+                if (snapshot.is_outdated) Nil
+                else snapshot.version.nodes.undefined_blobs.map(_.node)
+              }
+              else Nil
+
+            val files =
+              (thy_files ::: aux_files).filter(file =>
+                !loaded_buffer(file) && PIDE.resources.check_file(file))
 
             if (files.nonEmpty) {
               if (PIDE.options.bool("jedit_auto_load")) {