author | wenzelm |
Sat, 25 May 2013 17:40:44 +0200 | |
changeset 52147 | 9943f8067f11 |
parent 50566 | b43c4f660320 |
child 54509 | 1f77110c94ef |
permissions | -rw-r--r-- |
45007 | 1 |
/* Title: Tools/jEdit/src/jedit_thy_load.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 |
|
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
4 |
Primitives for loading theory files, based on jEdit buffer content. |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
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 |
package isabelle.jedit |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
8 |
|
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 |
import isabelle._ |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
11 |
|
48409 | 12 |
import java.io.{File => JFile, IOException} |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
13 |
import javax.swing.text.Segment |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
14 |
|
44963
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
15 |
import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSFile, VFSManager} |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
16 |
import org.gjt.sp.jedit.MiscUtilities |
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
17 |
import org.gjt.sp.jedit.{View, Buffer} |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
18 |
|
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
19 |
|
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48422
diff
changeset
|
20 |
class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax) |
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48422
diff
changeset
|
21 |
extends Thy_Load(loaded_theories, base_syntax) |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
22 |
{ |
50566
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
23 |
/* document node names */ |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
24 |
|
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
25 |
def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] = |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
26 |
Some(Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName)) |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
27 |
|
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
28 |
def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] = |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
29 |
{ |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
30 |
val name = JEdit_Lib.buffer_name(buffer) |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
31 |
Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory)) |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
32 |
} |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
33 |
|
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
34 |
|
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
35 |
/* file-system operations */ |
b43c4f660320
tuned signature: use thy_load to adapt to prover/editor specific view on sources;
wenzelm
parents:
49406
diff
changeset
|
36 |
|
44615 | 37 |
override def append(dir: String, source_path: Path): String = |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
38 |
{ |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
39 |
val path = source_path.expand |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
40 |
if (path.is_absolute) Isabelle_System.platform_path(path) |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
41 |
else { |
44615 | 42 |
val vfs = VFSManager.getVFSForPath(dir) |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
43 |
if (vfs.isInstanceOf[FileVFS]) |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
44 |
MiscUtilities.resolveSymlinks( |
44615 | 45 |
vfs.constructPath(dir, Isabelle_System.platform_path(path))) |
46 |
else vfs.constructPath(dir, Isabelle_System.standard_path(path)) |
|
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
47 |
} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
48 |
} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
49 |
|
48885 | 50 |
override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A = |
51 |
{ |
|
52 |
Swing_Thread.now { |
|
49406 | 53 |
JEdit_Lib.jedit_buffer(name.node) match { |
48885 | 54 |
case Some(buffer) => |
49406 | 55 |
JEdit_Lib.buffer_lock(buffer) { |
48885 | 56 |
Some(f(buffer.getSegment(0, buffer.getLength))) |
57 |
} |
|
58 |
case None => None |
|
59 |
} |
|
60 |
} getOrElse { |
|
61 |
val file = new JFile(name.node) // FIXME load URL via jEdit VFS (!?) |
|
62 |
if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) |
|
63 |
f(File.read(file)) |
|
64 |
} |
|
65 |
} |
|
66 |
||
44963
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
67 |
def check_file(view: View, path: String): Boolean = |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
68 |
{ |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
69 |
val vfs = VFSManager.getVFSForPath(path) |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
70 |
val session = vfs.createVFSSession(path, view) |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
71 |
|
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
72 |
try { |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
73 |
session != null && { |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
74 |
try { |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
75 |
val file = vfs._getFile(session, path, view) |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
76 |
file != null && file.isReadable && file.getType == VFSFile.FILE |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
77 |
} |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
78 |
catch { case _: IOException => false } |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
79 |
} |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
80 |
} |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
81 |
finally { |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
82 |
try { vfs._endVFSSession(session, view) } |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
83 |
catch { case _: IOException => } |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
84 |
} |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44953
diff
changeset
|
85 |
} |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
86 |
} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
87 |