author | wenzelm |
Thu, 01 Sep 2011 13:34:45 +0200 | |
changeset 44615 | a4ff8a787202 |
parent 44580 | 3bc9a215a56d |
child 44953 | cdfe42f1267c |
permissions | -rw-r--r-- |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/plugin.scala |
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 |
|
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
12 |
import java.io.File |
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 |
|
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
15 |
import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
16 |
import org.gjt.sp.jedit.MiscUtilities |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
17 |
|
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 |
class JEdit_Thy_Load extends Thy_Load |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
20 |
{ |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
21 |
/* loaded theories provided by prover */ |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
22 |
|
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
23 |
private var loaded_theories: Set[String] = Set() |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
24 |
|
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
25 |
override def register_thy(thy_name: String) |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
26 |
{ |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
27 |
synchronized { loaded_theories += thy_name } |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
28 |
} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
29 |
|
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
30 |
override def is_loaded(thy_name: String): Boolean = |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
31 |
synchronized { loaded_theories.contains(thy_name) } |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
32 |
|
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
33 |
|
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
34 |
/* file-system operations */ |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
35 |
|
44615 | 36 |
override def append(dir: String, source_path: Path): String = |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
37 |
{ |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
38 |
val path = source_path.expand |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
39 |
if (path.is_absolute) Isabelle_System.platform_path(path) |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
40 |
else { |
44615 | 41 |
val vfs = VFSManager.getVFSForPath(dir) |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
42 |
if (vfs.isInstanceOf[FileVFS]) |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
43 |
MiscUtilities.resolveSymlinks( |
44615 | 44 |
vfs.constructPath(dir, Isabelle_System.platform_path(path))) |
45 |
else vfs.constructPath(dir, Isabelle_System.standard_path(path)) |
|
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
46 |
} |
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 |
|
44615 | 49 |
override def check_thy(name: Document.Node.Name): Thy_Header = |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
50 |
{ |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
51 |
Swing_Thread.now { |
44615 | 52 |
Isabelle.jedit_buffer(name.node) match { |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
53 |
case Some(buffer) => |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
54 |
Isabelle.buffer_lock(buffer) { |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
55 |
val text = new Segment |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
56 |
buffer.getText(0, buffer.getLength, text) |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
57 |
Some(Thy_Header.read(text)) |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
58 |
} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
59 |
case None => None |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
60 |
} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
61 |
} getOrElse { |
44615 | 62 |
val file = new File(name.node) // FIXME load URL via jEdit VFS (!?) |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
63 |
if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString)) |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
64 |
Thy_Header.read(file) |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
65 |
} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
66 |
} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
67 |
} |
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
diff
changeset
|
68 |