author | wenzelm |
Wed, 09 Apr 2014 23:22:58 +0200 | |
changeset 56502 | db2836f65d42 |
parent 56460 | af28fdd50690 |
child 56666 | 229309cbc508 |
permissions | -rw-r--r-- |
56208 | 1 |
/* Title: Tools/jEdit/src/jedit_resources.scala |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
3 |
|
56208 | 4 |
Resources for theories and auxiliary files, based on jEdit buffer |
5 |
content and virtual file-systems. |
|
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
6 |
*/ |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
7 |
|
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
8 |
package isabelle.jedit |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
9 |
|
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
10 |
|
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
11 |
import isabelle._ |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
12 |
|
56502
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
13 |
import java.io.{File => JFile, ByteArrayOutputStream} |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
14 |
import javax.swing.text.Segment |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
15 |
|
56502
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
16 |
import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager} |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
17 |
import org.gjt.sp.jedit.MiscUtilities |
55134
1b67b17cdad5
propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents:
54517
diff
changeset
|
18 |
import org.gjt.sp.jedit.{jEdit, View, Buffer} |
54511 | 19 |
import org.gjt.sp.jedit.bufferio.BufferIORequest |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
20 |
|
56208 | 21 |
|
22 |
class JEdit_Resources(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax) |
|
23 |
extends Resources(loaded_theories, base_syntax) |
|
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
24 |
{ |
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
25 |
/* document node names */ |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
26 |
|
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
50566
diff
changeset
|
27 |
def node_name(buffer: Buffer): Document.Node.Name = |
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
28 |
{ |
54515 | 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) |
|
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
50566
diff
changeset
|
33 |
} |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
50566
diff
changeset
|
34 |
|
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
50566
diff
changeset
|
35 |
def theory_node_name(buffer: Buffer): Option[Document.Node.Name] = |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
50566
diff
changeset
|
36 |
{ |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
50566
diff
changeset
|
37 |
val name = node_name(buffer) |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
50566
diff
changeset
|
38 |
if (name.is_theory) Some(name) else None |
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
39 |
} |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
40 |
|
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
41 |
|
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
42 |
/* file-system operations */ |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
43 |
|
44615 | 44 |
override def append(dir: String, source_path: Path): String = |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
45 |
{ |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
46 |
val path = source_path.expand |
54517 | 47 |
if (dir == "" || path.is_absolute) Isabelle_System.platform_path(path) |
56502
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
48 |
else if (path.is_current) dir |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
49 |
else { |
44615 | 50 |
val vfs = VFSManager.getVFSForPath(dir) |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
51 |
if (vfs.isInstanceOf[FileVFS]) |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
52 |
MiscUtilities.resolveSymlinks( |
44615 | 53 |
vfs.constructPath(dir, Isabelle_System.platform_path(path))) |
54 |
else vfs.constructPath(dir, Isabelle_System.standard_path(path)) |
|
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
55 |
} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
56 |
} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
57 |
|
56502
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
58 |
override def with_thy_text[A](name: Document.Node.Name, consume: CharSequence => A): A = |
48885 | 59 |
{ |
60 |
Swing_Thread.now { |
|
56457
eea4bbe15745
tuned signature -- prefer static type Document.Node.Name;
wenzelm
parents:
56316
diff
changeset
|
61 |
JEdit_Lib.jedit_buffer(name) match { |
48885 | 62 |
case Some(buffer) => |
49406 | 63 |
JEdit_Lib.buffer_lock(buffer) { |
56502
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
64 |
Some(consume(buffer.getSegment(0, buffer.getLength))) |
48885 | 65 |
} |
66 |
case None => None |
|
67 |
} |
|
68 |
} getOrElse { |
|
56502
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
69 |
if (Url.is_wellformed(name.node)) consume(Url.read(name.node)) |
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
70 |
else { |
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
71 |
val file = new JFile(name.node) |
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
72 |
if (file.isFile) consume(File.read(file)) |
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
73 |
else error("No such file: " + quote(file.toString)) |
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
74 |
} |
48885 | 75 |
} |
76 |
} |
|
77 |
||
56502
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
78 |
def check_file(view: View, file: String): Boolean = |
44963
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
79 |
try { |
56502
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
80 |
if (Url.is_wellformed(file)) Url.is_readable(file) |
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
81 |
else (new JFile(file)).isFile |
44963
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
82 |
} |
56502
db2836f65d42
improved support for external URLs, based on standard Java network operations;
wenzelm
parents:
56460
diff
changeset
|
83 |
catch { case ERROR(_) => false } |
54511 | 84 |
|
85 |
||
86 |
/* file content */ |
|
87 |
||
88 |
def file_content(buffer: Buffer): Bytes = |
|
89 |
{ |
|
90 |
val path = buffer.getPath |
|
91 |
val vfs = VFSManager.getVFSForPath(path) |
|
92 |
val content = |
|
93 |
new BufferIORequest(null, buffer, null, vfs, path) { |
|
94 |
def _run() { } |
|
95 |
def apply(): Bytes = |
|
96 |
{ |
|
97 |
val out = |
|
98 |
new ByteArrayOutputStream(buffer.getLength + 1) { |
|
99 |
def content(): Bytes = Bytes(this.buf, 0, this.count) |
|
100 |
} |
|
101 |
write(buffer, out) |
|
102 |
out.content() |
|
103 |
} |
|
104 |
} |
|
105 |
content() |
|
106 |
} |
|
55134
1b67b17cdad5
propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents:
54517
diff
changeset
|
107 |
|
1b67b17cdad5
propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents:
54517
diff
changeset
|
108 |
|
1b67b17cdad5
propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents:
54517
diff
changeset
|
109 |
/* theory text edits */ |
1b67b17cdad5
propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
wenzelm
parents:
54517
diff
changeset
|
110 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
111 |
override def commit(change: Session.Change) |
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
112 |
{ |
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
113 |
if (change.syntax_changed) Swing_Thread.later { jEdit.propertiesChanged() } |
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
114 |
} |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
115 |
} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
116 |