explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
authorwenzelm
Sun Sep 18 13:47:12 2011 +0200 (2011-09-18)
changeset 449634662dddc2fd8
parent 44962 5554ed48b13f
child 44964 23dbab7f8cf4
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
src/Tools/jEdit/src/jedit_thy_load.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Sun Sep 18 13:39:33 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Sun Sep 18 13:47:12 2011 +0200
     1.3 @@ -9,11 +9,12 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import java.io.File
     1.8 +import java.io.{File, IOException}
     1.9  import javax.swing.text.Segment
    1.10  
    1.11 -import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
    1.12 +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
    1.13  import org.gjt.sp.jedit.MiscUtilities
    1.14 +import org.gjt.sp.jedit.View
    1.15  
    1.16  
    1.17  class JEdit_Thy_Load extends Thy_Load
    1.18 @@ -31,6 +32,26 @@
    1.19      }
    1.20    }
    1.21  
    1.22 +  def check_file(view: View, path: String): Boolean =
    1.23 +  {
    1.24 +    val vfs = VFSManager.getVFSForPath(path)
    1.25 +    val session = vfs.createVFSSession(path, view)
    1.26 +
    1.27 +    try {
    1.28 +      session != null && {
    1.29 +        try {
    1.30 +          val file = vfs._getFile(session, path, view)
    1.31 +          file != null && file.isReadable && file.getType == VFSFile.FILE
    1.32 +        }
    1.33 +        catch { case _: IOException => false }
    1.34 +      }
    1.35 +    }
    1.36 +    finally {
    1.37 +      try { vfs._endVFSSession(session, view) }
    1.38 +      catch { case _: IOException => }
    1.39 +    }
    1.40 +  }
    1.41 +
    1.42    override def check_thy(name: Document.Node.Name): Thy_Header =
    1.43    {
    1.44      Swing_Thread.now {
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Sep 18 13:39:33 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Sep 18 13:47:12 2011 +0200
     2.3 @@ -366,6 +366,8 @@
     2.4    private lazy val delay_load =
     2.5      Swing_Thread.delay_last(Isabelle.session.load_delay)
     2.6      {
     2.7 +      val view = jEdit.getActiveView()
     2.8 +
     2.9        val buffers = Isabelle.jedit_buffers().toList
    2.10        def loaded_buffer(name: String): Boolean =
    2.11          buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
    2.12 @@ -373,7 +375,8 @@
    2.13        val thys =
    2.14          for (buffer <- buffers; model <- Isabelle.document_model(buffer))
    2.15            yield model.name
    2.16 -      val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).filterNot(loaded_buffer _)
    2.17 +      val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).
    2.18 +        filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
    2.19  
    2.20        if (!files.isEmpty) {
    2.21          val files_list = new ListView(Library.sort_strings(files))
    2.22 @@ -381,7 +384,7 @@
    2.23            files_list.selection.indices += i
    2.24  
    2.25          val answer =
    2.26 -          Library.confirm_dialog(jEdit.getActiveView(),
    2.27 +          Library.confirm_dialog(view,
    2.28              "Auto loading of required files",
    2.29              JOptionPane.YES_NO_OPTION,
    2.30              "The following files are required to resolve theory imports.",
    2.31 @@ -390,7 +393,7 @@
    2.32          if (answer == 0)
    2.33            for {
    2.34              file <- files
    2.35 -            if !loaded_buffer(file) && files_list.selection.items.contains(file)
    2.36 +            if files_list.selection.items.contains(file)
    2.37            } jEdit.openFile(null: View, file)
    2.38        }
    2.39      }