|
1 /* |
|
2 * SideKick parser for Isabelle proof documents |
|
3 * |
|
4 * @author Fabian Immler, TU Munich |
|
5 * @author Makarius |
|
6 */ |
|
7 |
|
8 package isabelle.jedit |
|
9 |
|
10 import scala.collection.Set |
|
11 import scala.collection.immutable.TreeSet |
|
12 |
|
13 import javax.swing.tree.DefaultMutableTreeNode |
|
14 import javax.swing.text.Position |
|
15 import javax.swing.Icon |
|
16 |
|
17 import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} |
|
18 import errorlist.DefaultErrorSource |
|
19 import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} |
|
20 |
|
21 import isabelle.prover.{Command, Markup_Node} |
|
22 import isabelle.proofdocument.ProofDocument |
|
23 |
|
24 |
|
25 class IsabelleSideKickParser extends SideKickParser("isabelle") |
|
26 { |
|
27 /* parsing */ |
|
28 |
|
29 @volatile private var stopped = false |
|
30 override def stop() = { stopped = true } |
|
31 |
|
32 def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData = |
|
33 { |
|
34 implicit def int_to_pos(offset: Int): Position = |
|
35 new Position { def getOffset = offset; override def toString = offset.toString } |
|
36 |
|
37 stopped = false |
|
38 |
|
39 val data = new SideKickParsedData(buffer.getName) |
|
40 val root = data.root |
|
41 data.getAsset(root).setEnd(buffer.getLength) |
|
42 |
|
43 val prover_setup = Isabelle.prover_setup(buffer) |
|
44 if (prover_setup.isDefined) { |
|
45 val document = prover_setup.get.theory_view.current_document() |
|
46 for (command <- document.commands if !stopped) { |
|
47 root.add(command.markup_root(document).swing_tree((node: Markup_Node) => |
|
48 { |
|
49 val content = command.content(node.start, node.stop) |
|
50 val command_start = command.start(document) |
|
51 val id = command.id |
|
52 |
|
53 new DefaultMutableTreeNode(new IAsset { |
|
54 override def getIcon: Icon = null |
|
55 override def getShortString: String = content |
|
56 override def getLongString: String = node.info.toString |
|
57 override def getName: String = id |
|
58 override def setName(name: String) = () |
|
59 override def setStart(start: Position) = () |
|
60 override def getStart: Position = command_start + node.start |
|
61 override def setEnd(end: Position) = () |
|
62 override def getEnd: Position = command_start + node.stop |
|
63 override def toString = id + ": " + content + "[" + getStart + " - " + getEnd + "]" |
|
64 }) |
|
65 })) |
|
66 } |
|
67 if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>")) |
|
68 } |
|
69 else root.add(new DefaultMutableTreeNode("<buffer inactive>")) |
|
70 |
|
71 data |
|
72 } |
|
73 |
|
74 |
|
75 /* completion */ |
|
76 |
|
77 override def supportsCompletion = true |
|
78 override def canCompleteAnywhere = true |
|
79 |
|
80 override def complete(pane: EditPane, caret: Int): SideKickCompletion = |
|
81 { |
|
82 val buffer = pane.getBuffer |
|
83 |
|
84 val line = buffer.getLineOfOffset(caret) |
|
85 val start = buffer.getLineStartOffset(line) |
|
86 val text = buffer.getSegment(start, caret - start) |
|
87 |
|
88 val completion = |
|
89 Isabelle.prover_setup(buffer).map(_.prover.completion()).getOrElse(Isabelle.completion) |
|
90 |
|
91 completion.complete(text) match { |
|
92 case None => null |
|
93 case Some((word, cs)) => |
|
94 val ds = |
|
95 if (Isabelle_Encoding.is_active(buffer)) |
|
96 cs.map(Isabelle.system.symbols.decode(_)).sort(Completion.length_ord _) |
|
97 else cs |
|
98 new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } |
|
99 } |
|
100 } |
|
101 |
|
102 } |