12 import java.io.{File => JFile, 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, Buffer} |
18 |
18 |
19 |
19 |
20 class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax) |
20 class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax) |
21 extends Thy_Load(loaded_theories, base_syntax) |
21 extends Thy_Load(loaded_theories, base_syntax) |
22 { |
22 { |
|
23 /* document node names */ |
|
24 |
|
25 def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] = |
|
26 Some(Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName)) |
|
27 |
|
28 def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] = |
|
29 { |
|
30 val name = JEdit_Lib.buffer_name(buffer) |
|
31 Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory)) |
|
32 } |
|
33 |
|
34 |
|
35 /* file-system operations */ |
|
36 |
23 override def append(dir: String, source_path: Path): String = |
37 override def append(dir: String, source_path: Path): String = |
24 { |
38 { |
25 val path = source_path.expand |
39 val path = source_path.expand |
26 if (path.is_absolute) Isabelle_System.platform_path(path) |
40 if (path.is_absolute) Isabelle_System.platform_path(path) |
27 else { |
41 else { |