clarified undefined_blobs: already loaded theories are suppressed;
enabled jedit_auto_resolve (again): e.g. relevant for debugging when following links through source files;
--- 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
--- 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
--- 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()
}
}
--- 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
}
}