# HG changeset patch
# User wenzelm
# Date 1426278948 -3600
# Node ID f6ff191888425131ba66303f609d5c2d022c869a
# Parent  46b635624feb8f9b15719bd76f1d440fd96d55c5
tuned signature;
minimal I/O on GUI thread should be OK;

diff -r 46b635624feb -r f6ff19188842 src/Pure/PIDE/resources.scala
--- 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 */
 
diff -r 46b635624feb -r f6ff19188842 src/Tools/jEdit/src/jedit_resources.scala
--- 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 */
 
diff -r 46b635624feb -r f6ff19188842 src/Tools/jEdit/src/plugin.scala
--- 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")) {