author | wenzelm |
Sat, 20 Dec 2008 14:19:12 +0100 | |
changeset 34417 | bce2f2ea9819 |
parent 34408 | ad7b6c4813c8 |
permissions | -rw-r--r-- |
34393 | 1 |
/* |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
2 |
* SideKick parser for Isabelle proof documents |
34393 | 3 |
* |
34407 | 4 |
* @author Fabian Immler, TU Munich |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
5 |
* @author Makarius |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
6 |
* |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
7 |
* TODO: |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
8 |
* - locking of buffer and/or document model (!?) |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
9 |
* - check treatment of assets |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
10 |
* - completion support |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
11 |
* - rename to isabelle.jedit.IsabelleSideKickParser |
34393 | 12 |
*/ |
13 |
||
14 |
package isabelle.prover |
|
15 |
||
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
16 |
|
34393 | 17 |
import javax.swing.tree.DefaultMutableTreeNode |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
18 |
|
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
19 |
import isabelle.jedit.Plugin |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
20 |
|
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
21 |
import org.gjt.sp.jedit.{Buffer, EditPane} |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
22 |
import errorlist.DefaultErrorSource |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
23 |
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion} |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
24 |
|
34393 | 25 |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34401
diff
changeset
|
26 |
class IsabelleSKParser extends SideKickParser("isabelle") { |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
27 |
|
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
28 |
/* parsing */ |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
29 |
|
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
30 |
private var stopped = false |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
31 |
override def stop () = { stopped = true } |
34401
44241a37b74a
structure of markup-tree in scala, keep track of swing-nodes in background
immler@in.tum.de
parents:
34393
diff
changeset
|
32 |
|
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
33 |
def parse(buffer : Buffer, error_source : DefaultErrorSource): SideKickParsedData = { |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
34 |
stopped = false |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
35 |
|
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
36 |
val data = new SideKickParsedData(buffer.getName) |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
37 |
|
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
38 |
Plugin.plugin.prover_setup(buffer) match { |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
39 |
case None => |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
40 |
data.root.add(new DefaultMutableTreeNode("<buffer inactive>")) |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
41 |
case Some(prover_setup) => |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
42 |
val document = prover_setup.prover.document |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
43 |
val commands = document.commands() |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
44 |
while (!stopped && commands.hasNext) { |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
45 |
data.root.add(commands.next.root_node.swing_node) |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
46 |
} |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
47 |
if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>")) |
34393 | 48 |
} |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
49 |
|
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
50 |
data |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
51 |
} |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
52 |
|
34393 | 53 |
|
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
54 |
/* completion */ |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
55 |
|
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
56 |
override def supportsCompletion = true |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
57 |
override def canCompleteAnywhere = true |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
58 |
|
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
59 |
override def complete(pane: EditPane, caret: Int): SideKickCompletion = null |
34393 | 60 |
} |