src/Tools/jEdit/src/jedit_thy_load.scala
changeset 49424 0d2114eb412a
parent 47612 09ab89658a5d
child 49437 9613780a805b
     1.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Fri Jul 20 21:05:47 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Fri Jul 20 22:29:25 2012 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import java.io.{File, IOException}
     1.8 +import java.io.{File => JFile, IOException}
     1.9  import javax.swing.text.Segment
    1.10  
    1.11  import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager}
    1.12 @@ -65,7 +65,7 @@
    1.13          case None => None
    1.14        }
    1.15      } getOrElse {
    1.16 -      val file = new File(name.node)  // FIXME load URL via jEdit VFS (!?)
    1.17 +      val file = new JFile(name.node)  // FIXME load URL via jEdit VFS (!?)
    1.18        if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
    1.19        Thy_Header.read(file)
    1.20      }