author | wenzelm |
Sat, 05 Sep 2009 00:07:10 +0200 | |
changeset 34705 | cd2cdf3b33b9 |
parent 34704 | 504cab625d3e |
child 34717 | 3f32e08bbb6c |
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 |
34393 | 6 |
*/ |
7 |
||
34426
81f93e0f13b4
renamed isabelle.prover.IsabelleSKParser to isabelle.jedit.IsabelleSideKickParser;
wenzelm
parents:
34417
diff
changeset
|
8 |
package isabelle.jedit |
34393 | 9 |
|
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
10 |
import scala.collection.Set |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
11 |
import scala.collection.immutable.TreeSet |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
12 |
|
34393 | 13 |
import javax.swing.tree.DefaultMutableTreeNode |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
14 |
import javax.swing.text.Position |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
15 |
import javax.swing.Icon |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
16 |
|
34609
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset
|
17 |
import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
18 |
import errorlist.DefaultErrorSource |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
19 |
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
20 |
|
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
21 |
import isabelle.prover.{Command, MarkupNode} |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
22 |
import isabelle.proofdocument.ProofDocument |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
23 |
|
34393 | 24 |
|
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
25 |
class IsabelleSideKickParser extends SideKickParser("isabelle") |
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
26 |
{ |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
27 |
/* parsing */ |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
28 |
|
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
29 |
@volatile private var stopped = false |
34503 | 30 |
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
|
31 |
|
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
32 |
def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData = |
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
33 |
{ |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
34 |
stopped = false |
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
35 |
|
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
36 |
val data = new SideKickParsedData(buffer.getName) |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
37 |
|
34669 | 38 |
val prover_setup = Isabelle.prover_setup(buffer) |
34503 | 39 |
if (prover_setup.isDefined) { |
34650 | 40 |
val document = prover_setup.get.theory_view.current_document() |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
41 |
for (command <- document.commands if !stopped) { |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
42 |
data.root.add(command.markup_root(document). |
34704
504cab625d3e
simplified MarkupNode -- independent of Command and ProofDocument;
wenzelm
parents:
34703
diff
changeset
|
43 |
swing_tree((node: MarkupNode) => |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
44 |
{ |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
45 |
implicit def int2pos(offset: Int): Position = |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
46 |
new Position { def getOffset = offset; override def toString = offset.toString } |
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
47 |
|
34704
504cab625d3e
simplified MarkupNode -- independent of Command and ProofDocument;
wenzelm
parents:
34703
diff
changeset
|
48 |
val command_start = command.start(document) |
34705 | 49 |
val id = command.id |
50 |
||
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
51 |
new DefaultMutableTreeNode(new IAsset { |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
52 |
override def getIcon: Icon = null |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
53 |
override def getShortString: String = node.content |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
54 |
override def getLongString: String = node.info.toString |
34705 | 55 |
override def getName: String = id |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
56 |
override def setName(name: String) = () |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
57 |
override def setStart(start: Position) = () |
34704
504cab625d3e
simplified MarkupNode -- independent of Command and ProofDocument;
wenzelm
parents:
34703
diff
changeset
|
58 |
override def getStart: Position = command_start + node.start |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
59 |
override def setEnd(end: Position) = () |
34704
504cab625d3e
simplified MarkupNode -- independent of Command and ProofDocument;
wenzelm
parents:
34703
diff
changeset
|
60 |
override def getEnd: Position = command_start + node.stop |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
61 |
override def toString = |
34705 | 62 |
id + ": " + node.content + "[" + getStart + " - " + getEnd + "]" |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
63 |
}) |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
64 |
})) |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
65 |
} |
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
66 |
if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>")) |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
67 |
} |
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
68 |
else data.root.add(new DefaultMutableTreeNode("<buffer inactive>")) |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
69 |
|
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
70 |
data |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
71 |
} |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
72 |
|
34393 | 73 |
|
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
74 |
/* completion */ |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
75 |
|
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
76 |
override def supportsCompletion = true |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
77 |
override def canCompleteAnywhere = true |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
78 |
|
34609
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset
|
79 |
override def complete(pane: EditPane, caret: Int): SideKickCompletion = |
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset
|
80 |
{ |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
81 |
val buffer = pane.getBuffer |
34612
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
82 |
|
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
83 |
val line = buffer.getLineOfOffset(caret) |
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
84 |
val start = buffer.getLineStartOffset(line) |
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
85 |
val text = buffer.getSegment(start, caret - start) |
34609
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset
|
86 |
|
34612
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
87 |
val completion = |
34703 | 88 |
Isabelle.prover_setup(buffer).map(_.prover.completion).getOrElse(Isabelle.completion) |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
89 |
|
34612
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
90 |
completion.complete(text) match { |
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
91 |
case None => null |
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
92 |
case Some((word, cs)) => |
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
93 |
val ds = |
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
94 |
if (IsabelleEncoding.is_active(buffer)) |
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
95 |
cs.map(Isabelle.system.symbols.decode(_)).sort(Completion.length_ord _) |
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
96 |
else cs |
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
97 |
new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } |
34611 | 98 |
} |
34609
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset
|
99 |
} |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
100 |
|
34393 | 101 |
} |