# 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")) {