author | wenzelm |
Wed, 25 Aug 2010 11:13:27 +0200 | |
changeset 38663 | fcd56e6a04b9 |
parent 38658 | 20d82e98bcd7 |
child 39624 | 57496c868dcc |
permissions | -rw-r--r-- |
36760 | 1 |
/* Title: Tools/jEdit/src/jedit/isabelle_sidekick.scala |
2 |
Author: Fabian Immler, TU Munich |
|
3 |
Author: Makarius |
|
4 |
||
5 |
SideKick parsers for Isabelle proof documents. |
|
6 |
*/ |
|
34393 | 7 |
|
34426
81f93e0f13b4
renamed isabelle.prover.IsabelleSKParser to isabelle.jedit.IsabelleSideKickParser;
wenzelm
parents:
34417
diff
changeset
|
8 |
package isabelle.jedit |
34393 | 9 |
|
34760 | 10 |
|
36015 | 11 |
import isabelle._ |
12 |
||
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
13 |
import scala.collection.Set |
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
14 |
import scala.collection.immutable.TreeSet |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
15 |
|
34393 | 16 |
import javax.swing.tree.DefaultMutableTreeNode |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
17 |
import javax.swing.text.Position |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
18 |
import javax.swing.Icon |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
19 |
|
34609
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset
|
20 |
import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
21 |
import errorlist.DefaultErrorSource |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
22 |
import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} |
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
23 |
|
34393 | 24 |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
25 |
object Isabelle_Sidekick |
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
26 |
{ |
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
27 |
implicit def int_to_pos(offset: Int): Position = |
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
28 |
new Position { def getOffset = offset; override def toString = offset.toString } |
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
29 |
} |
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
30 |
|
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
31 |
|
36759 | 32 |
abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name) |
34625
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 |
/* parsing */ |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
35 |
|
36759 | 36 |
@volatile protected var stopped = false |
34503 | 37 |
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
|
38 |
|
36759 | 39 |
def parser(data: SideKickParsedData, model: Document_Model): Unit |
40 |
||
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
41 |
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
|
42 |
{ |
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
43 |
import Isabelle_Sidekick.int_to_pos |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34705
diff
changeset
|
44 |
|
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
45 |
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
|
46 |
|
38640 | 47 |
// FIXME lock buffer (!??) |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
48 |
val data = new SideKickParsedData(buffer.getName) |
34717
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34705
diff
changeset
|
49 |
val root = data.root |
3f32e08bbb6c
sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents:
34705
diff
changeset
|
50 |
data.getAsset(root).setEnd(buffer.getLength) |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
51 |
|
34789 | 52 |
Swing_Thread.now { Document_Model(buffer) } match { |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34777
diff
changeset
|
53 |
case Some(model) => |
36759 | 54 |
parser(data, model) |
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset
|
55 |
if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>")) |
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34760
diff
changeset
|
56 |
case None => root.add(new DefaultMutableTreeNode("<buffer inactive>")) |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
57 |
} |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
58 |
data |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
59 |
} |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
60 |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
61 |
|
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
62 |
/* completion */ |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
63 |
|
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
64 |
override def supportsCompletion = true |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
65 |
override def canCompleteAnywhere = true |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
66 |
|
34609
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset
|
67 |
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
|
68 |
{ |
38640 | 69 |
// FIXME lock buffer (!?) |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
70 |
val buffer = pane.getBuffer |
34612
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
71 |
|
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
72 |
val line = buffer.getLineOfOffset(caret) |
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
73 |
val start = buffer.getLineStartOffset(line) |
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
74 |
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
|
75 |
|
38569 | 76 |
val completion = Isabelle.session.current_syntax().completion |
34475
f963335dbc6b
implemented IsabelleSideKickParser.complete
immler@in.tum.de
parents:
34440
diff
changeset
|
77 |
|
34612
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
78 |
completion.complete(text) match { |
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
79 |
case None => null |
5a03dc7a19e1
fall back on Isabelle system completion (symbols only);
wenzelm
parents:
34611
diff
changeset
|
80 |
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
|
81 |
val ds = |
35004
b89a31957950
filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents:
34871
diff
changeset
|
82 |
(if (Isabelle_Encoding.is_active(buffer)) |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38426
diff
changeset
|
83 |
cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _) |
35004
b89a31957950
filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents:
34871
diff
changeset
|
84 |
else cs).filter(_ != word) |
b89a31957950
filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents:
34871
diff
changeset
|
85 |
if (ds.isEmpty) null |
b89a31957950
filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents:
34871
diff
changeset
|
86 |
else new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } |
34611 | 87 |
} |
34609
7ca1ef2f150d
simplified and reactivated SideKickCompletion, cf. org.gjt.sp.jedit.gui.CompleteWord;
wenzelm
parents:
34562
diff
changeset
|
88 |
} |
34393 | 89 |
} |
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
90 |
|
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
91 |
|
36759 | 92 |
class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle") |
93 |
{ |
|
94 |
def parser(data: SideKickParsedData, model: Document_Model) |
|
95 |
{ |
|
96 |
import Isabelle_Sidekick.int_to_pos |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
97 |
|
36759 | 98 |
val root = data.root |
38417 | 99 |
val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) |
36759 | 100 |
for { |
38569 | 101 |
(command, command_start) <- snapshot.node.command_range() |
36762 | 102 |
if command.is_command && !stopped |
36759 | 103 |
} |
104 |
{ |
|
105 |
val name = command.name |
|
106 |
val node = |
|
107 |
new DefaultMutableTreeNode(new IAsset { |
|
108 |
override def getIcon: Icon = null |
|
109 |
override def getShortString: String = name |
|
110 |
override def getLongString: String = name |
|
111 |
override def getName: String = name |
|
112 |
override def setName(name: String) = () |
|
113 |
override def setStart(start: Position) = () |
|
114 |
override def getStart: Position = command_start |
|
115 |
override def setEnd(end: Position) = () |
|
116 |
override def getEnd: Position = command_start + command.length |
|
38417 | 117 |
override def toString = name}) |
36759 | 118 |
root.add(node) |
119 |
} |
|
120 |
} |
|
121 |
} |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
122 |
|
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
123 |
|
36759 | 124 |
class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw") |
125 |
{ |
|
126 |
def parser(data: SideKickParsedData, model: Document_Model) |
|
127 |
{ |
|
128 |
import Isabelle_Sidekick.int_to_pos |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
129 |
|
36759 | 130 |
val root = data.root |
38223 | 131 |
val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) |
38569 | 132 |
for ((command, command_start) <- snapshot.node.command_range() if !stopped) { |
38658 | 133 |
snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) => |
36759 | 134 |
{ |
38663 | 135 |
val range = info.range + command_start |
38577 | 136 |
val content = command.source(info.range).replace('\n', ' ') |
38663 | 137 |
val info_text = |
138 |
info.info match { |
|
139 |
case elem @ XML.Elem(_, _) => |
|
140 |
Pretty.formatted(List(elem), margin = 40).mkString("\n") |
|
141 |
case x => x.toString |
|
142 |
} |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
143 |
|
36759 | 144 |
new DefaultMutableTreeNode(new IAsset { |
145 |
override def getIcon: Icon = null |
|
146 |
override def getShortString: String = content |
|
38663 | 147 |
override def getLongString: String = info_text |
148 |
override def getName: String = command.toString |
|
36759 | 149 |
override def setName(name: String) = () |
150 |
override def setStart(start: Position) = () |
|
38663 | 151 |
override def getStart: Position = range.start |
36759 | 152 |
override def setEnd(end: Position) = () |
38663 | 153 |
override def getEnd: Position = range.stop |
154 |
override def toString = "\"" + content + "\" " + range.toString |
|
36759 | 155 |
}) |
38479
e628da370072
more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents:
38426
diff
changeset
|
156 |
}) |
36759 | 157 |
} |
158 |
} |
|
159 |
} |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
160 |