# HG changeset patch
# User wenzelm
# Date 1316346432 -7200
# Node ID 4662dddc2fd83672b742007b71b04b74a5ba7c8c
# Parent  5554ed48b13f2948bc54a1e7d247d15bd8da05a6
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;

diff -r 5554ed48b13f -r 4662dddc2fd8 src/Tools/jEdit/src/jedit_thy_load.scala
--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Sun Sep 18 13:39:33 2011 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Sun Sep 18 13:47:12 2011 +0200
@@ -9,11 +9,12 @@
 
 import isabelle._
 
-import java.io.File
+import java.io.{File, IOException}
 import javax.swing.text.Segment
 
-import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
+import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
 import org.gjt.sp.jedit.MiscUtilities
+import org.gjt.sp.jedit.View
 
 
 class JEdit_Thy_Load extends Thy_Load
@@ -31,6 +32,26 @@
     }
   }
 
+  def check_file(view: View, path: String): Boolean =
+  {
+    val vfs = VFSManager.getVFSForPath(path)
+    val session = vfs.createVFSSession(path, view)
+
+    try {
+      session != null && {
+        try {
+          val file = vfs._getFile(session, path, view)
+          file != null && file.isReadable && file.getType == VFSFile.FILE
+        }
+        catch { case _: IOException => false }
+      }
+    }
+    finally {
+      try { vfs._endVFSSession(session, view) }
+      catch { case _: IOException => }
+    }
+  }
+
   override def check_thy(name: Document.Node.Name): Thy_Header =
   {
     Swing_Thread.now {
diff -r 5554ed48b13f -r 4662dddc2fd8 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Sep 18 13:39:33 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sun Sep 18 13:47:12 2011 +0200
@@ -366,6 +366,8 @@
   private lazy val delay_load =
     Swing_Thread.delay_last(Isabelle.session.load_delay)
     {
+      val view = jEdit.getActiveView()
+
       val buffers = Isabelle.jedit_buffers().toList
       def loaded_buffer(name: String): Boolean =
         buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
@@ -373,7 +375,8 @@
       val thys =
         for (buffer <- buffers; model <- Isabelle.document_model(buffer))
           yield model.name
-      val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).filterNot(loaded_buffer _)
+      val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).
+        filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
 
       if (!files.isEmpty) {
         val files_list = new ListView(Library.sort_strings(files))
@@ -381,7 +384,7 @@
           files_list.selection.indices += i
 
         val answer =
-          Library.confirm_dialog(jEdit.getActiveView(),
+          Library.confirm_dialog(view,
             "Auto loading of required files",
             JOptionPane.YES_NO_OPTION,
             "The following files are required to resolve theory imports.",
@@ -390,7 +393,7 @@
         if (answer == 0)
           for {
             file <- files
-            if !loaded_buffer(file) && files_list.selection.items.contains(file)
+            if files_list.selection.items.contains(file)
           } jEdit.openFile(null: View, file)
       }
     }