|
1 /* Title: Tools/jEdit/src/jedit_resources.scala |
|
2 Author: Makarius |
|
3 |
|
4 Resources for theories and auxiliary files, based on jEdit buffer |
|
5 content and virtual file-systems. |
|
6 */ |
|
7 |
|
8 package isabelle.jedit |
|
9 |
|
10 |
|
11 import isabelle._ |
|
12 |
|
13 import java.io.{File => JFile, IOException, ByteArrayOutputStream} |
|
14 import javax.swing.text.Segment |
|
15 |
|
16 import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager} |
|
17 import org.gjt.sp.jedit.MiscUtilities |
|
18 import org.gjt.sp.jedit.{jEdit, View, Buffer} |
|
19 import org.gjt.sp.jedit.bufferio.BufferIORequest |
|
20 |
|
21 |
|
22 class JEdit_Resources(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax) |
|
23 extends Resources(loaded_theories, base_syntax) |
|
24 { |
|
25 /* document node names */ |
|
26 |
|
27 def node_name(buffer: Buffer): Document.Node.Name = |
|
28 { |
|
29 val node = JEdit_Lib.buffer_name(buffer) |
|
30 val theory = Thy_Header.thy_name(node).getOrElse("") |
|
31 val master_dir = if (theory == "") "" else buffer.getDirectory |
|
32 Document.Node.Name(node, master_dir, theory) |
|
33 } |
|
34 |
|
35 def theory_node_name(buffer: Buffer): Option[Document.Node.Name] = |
|
36 { |
|
37 val name = node_name(buffer) |
|
38 if (name.is_theory) Some(name) else None |
|
39 } |
|
40 |
|
41 |
|
42 /* file-system operations */ |
|
43 |
|
44 override def append(dir: String, source_path: Path): String = |
|
45 { |
|
46 val path = source_path.expand |
|
47 if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path) |
|
48 else { |
|
49 val vfs = VFSManager.getVFSForPath(dir) |
|
50 if (vfs.isInstanceOf[FileVFS]) |
|
51 MiscUtilities.resolveSymlinks( |
|
52 vfs.constructPath(dir, Isabelle_System.platform_path(path))) |
|
53 else vfs.constructPath(dir, Isabelle_System.standard_path(path)) |
|
54 } |
|
55 } |
|
56 |
|
57 override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = |
|
58 { |
|
59 Swing_Thread.now { |
|
60 JEdit_Lib.jedit_buffer(name.node) match { |
|
61 case Some(buffer) => |
|
62 JEdit_Lib.buffer_lock(buffer) { |
|
63 Some(f(buffer.getSegment(0, buffer.getLength))) |
|
64 } |
|
65 case None => None |
|
66 } |
|
67 } getOrElse { |
|
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)) |
|
70 f(File.read(file)) |
|
71 } |
|
72 } |
|
73 |
|
74 def check_file(view: View, path: String): Boolean = |
|
75 { |
|
76 val vfs = VFSManager.getVFSForPath(path) |
|
77 val session = vfs.createVFSSession(path, view) |
|
78 |
|
79 try { |
|
80 session != null && { |
|
81 try { |
|
82 val file = vfs._getFile(session, path, view) |
|
83 file != null && file.isReadable && file.getType == VFSFile.FILE |
|
84 } |
|
85 catch { case _: IOException => false } |
|
86 } |
|
87 } |
|
88 finally { |
|
89 try { vfs._endVFSSession(session, view) } |
|
90 catch { case _: IOException => } |
|
91 } |
|
92 } |
|
93 |
|
94 |
|
95 /* file content */ |
|
96 |
|
97 def file_content(buffer: Buffer): Bytes = |
|
98 { |
|
99 val path = buffer.getPath |
|
100 val vfs = VFSManager.getVFSForPath(path) |
|
101 val content = |
|
102 new BufferIORequest(null, buffer, null, vfs, path) { |
|
103 def _run() { } |
|
104 def apply(): Bytes = |
|
105 { |
|
106 val out = |
|
107 new ByteArrayOutputStream(buffer.getLength + 1) { |
|
108 def content(): Bytes = Bytes(this.buf, 0, this.count) |
|
109 } |
|
110 write(buffer, out) |
|
111 out.content() |
|
112 } |
|
113 } |
|
114 content() |
|
115 } |
|
116 |
|
117 |
|
118 /* theory text edits */ |
|
119 |
|
120 override def syntax_changed(): Unit = |
|
121 Swing_Thread.later { jEdit.propertiesChanged() } |
|
122 } |
|
123 |