equal
deleted
inserted
replaced
7 package isabelle.jedit |
7 package isabelle.jedit |
8 |
8 |
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import java.io.{File, IOException} |
12 import java.io.{File => JFile, IOException} |
13 import javax.swing.text.Segment |
13 import javax.swing.text.Segment |
14 |
14 |
15 import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager} |
15 import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager} |
16 import org.gjt.sp.jedit.MiscUtilities |
16 import org.gjt.sp.jedit.MiscUtilities |
17 import org.gjt.sp.jedit.View |
17 import org.gjt.sp.jedit.View |
63 Some(Thy_Header.read(text)) |
63 Some(Thy_Header.read(text)) |
64 } |
64 } |
65 case None => None |
65 case None => None |
66 } |
66 } |
67 } getOrElse { |
67 } getOrElse { |
68 val file = new File(name.node) // FIXME load URL via jEdit VFS (!?) |
68 val file = new JFile(name.node) // FIXME load URL via jEdit VFS (!?) |
69 if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) |
69 if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) |
70 Thy_Header.read(file) |
70 Thy_Header.read(file) |
71 } |
71 } |
72 } |
72 } |
73 } |
73 } |