--- a/src/Pure/PIDE/resources.scala Fri Mar 13 16:09:55 2015 +0100
+++ b/src/Pure/PIDE/resources.scala Fri Mar 13 21:35:48 2015 +0100
@@ -110,6 +110,13 @@
def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
with_thy_reader(name, check_thy_reader(qualifier, name, _))
+ def check_file(file: String): Boolean =
+ try {
+ if (Url.is_wellformed(file)) Url.is_readable(file)
+ else (new JFile(file)).isFile
+ }
+ catch { case ERROR(_) => false }
+
/* document changes */
--- a/src/Tools/jEdit/src/jedit_resources.scala Fri Mar 13 16:09:55 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Fri Mar 13 21:35:48 2015 +0100
@@ -79,13 +79,6 @@
}
}
- def check_file(view: View, file: String): Boolean =
- try {
- if (Url.is_wellformed(file)) Url.is_readable(file)
- else (new JFile(file)).isFile
- }
- catch { case ERROR(_) => false }
-
/* file content */
--- a/src/Tools/jEdit/src/plugin.scala Fri Mar 13 16:09:55 2015 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Mar 13 21:35:48 2015 +0100
@@ -216,9 +216,8 @@
} yield (model.node_name, Position.none)
val thy_info = new Thy_Info(PIDE.resources)
- // FIXME avoid I/O on GUI thread!?!
val files = thy_info.dependencies("", thys).deps.map(_.name.node).
- filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
+ filter(file => !loaded_buffer(file) && PIDE.resources.check_file(file))
if (files.nonEmpty) {
if (PIDE.options.bool("jedit_auto_load")) {