tuned signature;
authorwenzelm
Fri Mar 13 21:35:48 2015 +0100 (2015-03-13 ago)
changeset 59691f6ff19188842
parent 59690 46b635624feb
child 59692 03aa1b63af10
tuned signature;
minimal I/O on GUI thread should be OK;
src/Pure/PIDE/resources.scala
src/Tools/jEdit/src/jedit_resources.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Fri Mar 13 16:09:55 2015 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Fri Mar 13 21:35:48 2015 +0100
     1.3 @@ -110,6 +110,13 @@
     1.4    def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
     1.5      with_thy_reader(name, check_thy_reader(qualifier, name, _))
     1.6  
     1.7 +  def check_file(file: String): Boolean =
     1.8 +    try {
     1.9 +      if (Url.is_wellformed(file)) Url.is_readable(file)
    1.10 +      else (new JFile(file)).isFile
    1.11 +    }
    1.12 +    catch { case ERROR(_) => false }
    1.13 +
    1.14  
    1.15    /* document changes */
    1.16  
     2.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Fri Mar 13 16:09:55 2015 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Fri Mar 13 21:35:48 2015 +0100
     2.3 @@ -79,13 +79,6 @@
     2.4      }
     2.5    }
     2.6  
     2.7 -  def check_file(view: View, file: String): Boolean =
     2.8 -    try {
     2.9 -      if (Url.is_wellformed(file)) Url.is_readable(file)
    2.10 -      else (new JFile(file)).isFile
    2.11 -    }
    2.12 -    catch { case ERROR(_) => false }
    2.13 -
    2.14  
    2.15    /* file content */
    2.16  
     3.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Mar 13 16:09:55 2015 +0100
     3.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Mar 13 21:35:48 2015 +0100
     3.3 @@ -216,9 +216,8 @@
     3.4                } yield (model.node_name, Position.none)
     3.5  
     3.6              val thy_info = new Thy_Info(PIDE.resources)
     3.7 -            // FIXME avoid I/O on GUI thread!?!
     3.8              val files = thy_info.dependencies("", thys).deps.map(_.name.node).
     3.9 -              filter(file => !loaded_buffer(file) && PIDE.resources.check_file(view, file))
    3.10 +              filter(file => !loaded_buffer(file) && PIDE.resources.check_file(file))
    3.11  
    3.12              if (files.nonEmpty) {
    3.13                if (PIDE.options.bool("jedit_auto_load")) {