author | wenzelm |
Sat, 24 Dec 2022 13:19:39 +0100 | |
changeset 76768 | 40c8275f0131 |
parent 76765 | c654103e9c9d |
child 77504 | fd40e36045fd |
permissions | -rw-r--r-- |
43282
5d294220ca43
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents:
40792
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/isabelle_sidekick.scala |
36760 | 2 |
Author: Fabian Immler, TU Munich |
3 |
Author: Makarius |
|
4 |
||
5 |
SideKick parsers for Isabelle proof documents. |
|
6 |
*/ |
|
34393 | 7 |
|
73987
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
8 |
package isabelle.jedit_main |
34393 | 9 |
|
34760 | 10 |
|
36015 | 11 |
import isabelle._ |
73987
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
12 |
import isabelle.jedit._ |
36015 | 13 |
|
34393 | 14 |
import javax.swing.tree.DefaultMutableTreeNode |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
15 |
import javax.swing.text.Position |
74037 | 16 |
import javax.swing.Icon |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
17 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
18 |
import org.gjt.sp.jedit.Buffer |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
19 |
import sidekick.{SideKickParser, SideKickParsedData, IAsset} |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
20 |
|
34393 | 21 |
|
75393 | 22 |
object Isabelle_Sidekick { |
40477 | 23 |
def int_to_pos(offset: Text.Offset): Position = |
74037 | 24 |
new Position { |
25 |
def getOffset: Text.Offset = offset |
|
26 |
override def toString: String = offset.toString |
|
27 |
} |
|
40452
45e7c2889d2f
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents:
39624
diff
changeset
|
28 |
|
75393 | 29 |
def root_data(buffer: Buffer): SideKickParsedData = { |
58526 | 30 |
val data = new SideKickParsedData(buffer.getName) |
31 |
data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength)) |
|
32 |
data |
|
33 |
} |
|
34 |
||
75393 | 35 |
class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset { |
69377 | 36 |
private val css = GUI.imitate_font_css(GUI.label_font()) |
59183
ec83638b6bfb
imitate font more carefully: err on smaller size;
wenzelm
parents:
59091
diff
changeset
|
37 |
|
74037 | 38 |
protected var _name: String = text |
39 |
protected var _start: Position = int_to_pos(range.start) |
|
40 |
protected var _end: Position = int_to_pos(range.stop) |
|
40452
45e7c2889d2f
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents:
39624
diff
changeset
|
41 |
override def getIcon: Icon = null |
75393 | 42 |
override def getShortString: String = { |
59933 | 43 |
val n = keyword.length |
44 |
val s = |
|
45 |
_name.indexOf(keyword) match { |
|
46 |
case i if i >= 0 && n > 0 => |
|
62113 | 47 |
HTML.output(_name.substring(0, i)) + |
48 |
"<b>" + HTML.output(keyword) + "</b>" + |
|
49 |
HTML.output(_name.substring(i + n)) |
|
50 |
case _ => HTML.output(_name) |
|
59933 | 51 |
} |
52 |
"<html><span style=\"" + css + "\">" + s + "</span></html>" |
|
53 |
} |
|
40452
45e7c2889d2f
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents:
39624
diff
changeset
|
54 |
override def getLongString: String = _name |
45e7c2889d2f
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents:
39624
diff
changeset
|
55 |
override def getName: String = _name |
71601 | 56 |
override def setName(name: String): Unit = _name = name |
40452
45e7c2889d2f
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents:
39624
diff
changeset
|
57 |
override def getStart: Position = _start |
71601 | 58 |
override def setStart(start: Position): Unit = _start = start |
40452
45e7c2889d2f
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents:
39624
diff
changeset
|
59 |
override def getEnd: Position = _end |
71601 | 60 |
override def setEnd(end: Position): Unit = _end = end |
57912 | 61 |
override def toString: String = _name |
40452
45e7c2889d2f
misc tuning and simplification, using Isabelle_Sidekick.Asset (not sidekick.Asset, which is dynamically dispatched to slightly different semantics);
wenzelm
parents:
39624
diff
changeset
|
62 |
} |
51618
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
63 |
|
58747 | 64 |
class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range) |
65 |
||
75393 | 66 |
def swing_markup_tree( |
67 |
tree: Markup_Tree, |
|
68 |
parent: DefaultMutableTreeNode, |
|
69 |
swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode |
|
70 |
): Unit = { |
|
51618
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
71 |
for ((_, entry) <- tree.branches) { |
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
72 |
val node = swing_node(Text.Info(entry.range, entry.markup)) |
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
73 |
swing_markup_tree(entry.subtree, node, swing_node) |
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
74 |
parent.add(node) |
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
75 |
} |
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
76 |
} |
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
77 |
} |
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
78 |
|
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
79 |
|
75393 | 80 |
class Isabelle_Sidekick(name: String) extends SideKickParser(name) { |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
81 |
override def supportsCompletion = false |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
82 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
83 |
|
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
84 |
/* parsing */ |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
85 |
|
36759 | 86 |
@volatile protected var stopped = false |
74037 | 87 |
override def stop(): Unit = { 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
|
88 |
|
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
89 |
def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false |
36759 | 90 |
|
75393 | 91 |
def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = { |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
92 |
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
|
93 |
|
38640 | 94 |
// FIXME lock buffer (!??) |
58526 | 95 |
val data = Isabelle_Sidekick.root_data(buffer) |
60272
4f72b00d9952
no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;
wenzelm
parents:
59933
diff
changeset
|
96 |
val syntax = Isabelle.buffer_syntax(buffer) |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
97 |
val ok = |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
98 |
if (syntax.isDefined) { |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
99 |
val ok = parser(buffer, syntax.get, data) |
58526 | 100 |
if (stopped) { data.root.add(new DefaultMutableTreeNode("<stopped>")); true } |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
101 |
else ok |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
102 |
} |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
103 |
else false |
58526 | 104 |
if (!ok) data.root.add(new DefaultMutableTreeNode("<ignored>")) |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
105 |
|
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
106 |
data |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
107 |
} |
34393 | 108 |
} |
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
109 |
|
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
110 |
|
48718 | 111 |
class Isabelle_Sidekick_Structure( |
75393 | 112 |
name: String, |
113 |
node_name: Buffer => Option[Document.Node.Name], |
|
114 |
parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document] |
|
115 |
) extends Isabelle_Sidekick(name) { |
|
116 |
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { |
|
58743 | 117 |
def make_tree( |
118 |
parent: DefaultMutableTreeNode, |
|
119 |
offset: Text.Offset, |
|
75393 | 120 |
documents: List[Document_Structure.Document] |
121 |
): Unit = { |
|
73359 | 122 |
documents.foldLeft(offset) { |
123 |
case (i, document) => |
|
124 |
document match { |
|
125 |
case Document_Structure.Block(name, text, body) => |
|
126 |
val range = Text.Range(i, i + document.length) |
|
127 |
val node = |
|
128 |
new DefaultMutableTreeNode( |
|
129 |
new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range)) |
|
130 |
parent.add(node) |
|
131 |
make_tree(node, i, body) |
|
132 |
case _ => |
|
133 |
} |
|
134 |
i + document.length |
|
40455
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
135 |
} |
58743 | 136 |
} |
40455
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
137 |
|
48718 | 138 |
node_name(buffer) match { |
139 |
case Some(name) => |
|
63606 | 140 |
make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer))) |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
141 |
true |
63606 | 142 |
case None => |
143 |
false |
|
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
144 |
} |
36759 | 145 |
} |
146 |
} |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
147 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
148 |
class Isabelle_Sidekick_Default extends |
63606 | 149 |
Isabelle_Sidekick_Structure("isabelle", |
71601 | 150 |
PIDE.resources.theory_node_name, Document_Structure.parse_sections) |
63606 | 151 |
|
152 |
class Isabelle_Sidekick_Context extends |
|
153 |
Isabelle_Sidekick_Structure("isabelle-context", |
|
71601 | 154 |
PIDE.resources.theory_node_name, Document_Structure.parse_blocks) |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
155 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
156 |
class Isabelle_Sidekick_Options extends |
63606 | 157 |
Isabelle_Sidekick_Structure("isabelle-options", |
71601 | 158 |
_ => Some(Document.Node.Name("options")), Document_Structure.parse_sections) |
48718 | 159 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
160 |
class Isabelle_Sidekick_Root extends |
63606 | 161 |
Isabelle_Sidekick_Structure("isabelle-root", |
71601 | 162 |
_ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections) |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
163 |
|
63610 | 164 |
class Isabelle_Sidekick_ML extends |
165 |
Isabelle_Sidekick_Structure("isabelle-ml", |
|
166 |
buffer => Some(PIDE.resources.node_name(buffer)), |
|
167 |
(_, _, text) => Document_Structure.parse_ml_sections(false, text)) |
|
168 |
||
169 |
class Isabelle_Sidekick_SML extends |
|
170 |
Isabelle_Sidekick_Structure("isabelle-sml", |
|
171 |
buffer => Some(PIDE.resources.node_name(buffer)), |
|
172 |
(_, _, text) => Document_Structure.parse_ml_sections(true, text)) |
|
173 |
||
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
174 |
|
75393 | 175 |
class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup") { |
176 |
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { |
|
55513
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
177 |
val opt_snapshot = |
76768
40c8275f0131
tuned signature: follow terminology of VSCode_Resources;
wenzelm
parents:
76765
diff
changeset
|
178 |
Document_Model.get_model(buffer) match { |
76765
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
75394
diff
changeset
|
179 |
case Some(model) if model.is_theory => Some(Document_Model.snapshot(model)) |
60272
4f72b00d9952
no GUI_Thread for SideKick parsers (in contrast to 4c8205fe3644), to avoid danger of deadlock due to nested context switch;
wenzelm
parents:
59933
diff
changeset
|
180 |
case _ => None |
55513
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
181 |
} |
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
182 |
opt_snapshot match { |
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
183 |
case Some(snapshot) => |
56373
0605d90be6fc
tuned signature -- more explicit iterator terminology;
wenzelm
parents:
56301
diff
changeset
|
184 |
for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) { |
55650 | 185 |
val markup = |
56301
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56299
diff
changeset
|
186 |
snapshot.state.command_markup( |
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56299
diff
changeset
|
187 |
snapshot.version, command, Command.Markup_Index.markup, |
56743 | 188 |
command.range, Markup.Elements.full) |
58526 | 189 |
Isabelle_Sidekick.swing_markup_tree(markup, data.root, |
75394 | 190 |
{ (info: Text.Info[List[XML.Elem]]) => |
75393 | 191 |
val range = info.range + command_start |
192 |
val content = command.source(info.range).replace('\n', ' ') |
|
193 |
val info_text = Pretty.formatted(Pretty.fbreaks(info.info), margin = 40.0).mkString |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
194 |
|
75393 | 195 |
new DefaultMutableTreeNode( |
196 |
new Isabelle_Sidekick.Asset(command.toString, range) { |
|
197 |
override def getShortString: String = content |
|
198 |
override def getLongString: String = info_text |
|
199 |
override def toString: String = quote(content) + " " + range.toString |
|
200 |
}) |
|
201 |
}) |
|
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
202 |
} |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
203 |
true |
55513
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
204 |
case None => false |
36759 | 205 |
} |
206 |
} |
|
207 |
} |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
208 |
|
52539 | 209 |
|
75393 | 210 |
class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news") { |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
211 |
private val Heading1 = """^New in (.*)\w*$""".r |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
212 |
private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r |
52539 | 213 |
|
214 |
private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode = |
|
58747 | 215 |
new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop))) |
52539 | 216 |
|
75393 | 217 |
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { |
52539 | 218 |
var offset = 0 |
58542 | 219 |
var end_offset = 0 |
220 |
||
221 |
var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None |
|
222 |
var start2: Option[(Int, String)] = None |
|
223 |
||
74037 | 224 |
def close1(): Unit = |
58542 | 225 |
start1 match { |
226 |
case Some((start_offset, s, body)) => |
|
227 |
val node = make_node(s, start_offset, end_offset) |
|
228 |
body.foreach(node.add(_)) |
|
229 |
data.root.add(node) |
|
230 |
start1 = None |
|
231 |
case None => |
|
232 |
} |
|
233 |
||
74037 | 234 |
def close2(): Unit = |
58542 | 235 |
start2 match { |
236 |
case Some((start_offset, s)) => |
|
237 |
start1 match { |
|
238 |
case Some((start_offset1, s1, body)) => |
|
239 |
val node = make_node(s, start_offset, end_offset) |
|
240 |
start1 = Some((start_offset1, s1, body :+ node)) |
|
241 |
case None => |
|
242 |
} |
|
243 |
start2 = None |
|
244 |
case None => |
|
245 |
} |
|
52539 | 246 |
|
247 |
for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) { |
|
248 |
line match { |
|
74037 | 249 |
case Heading1(s) => close2(); close1(); start1 = Some((offset, s, Vector())) |
250 |
case Heading2(s) => close2(); start2 = Some((offset, s)) |
|
52539 | 251 |
case _ => |
252 |
} |
|
253 |
offset += line.length + 1 |
|
71601 | 254 |
if (!line.forall(Character.isSpaceChar)) end_offset = offset |
52539 | 255 |
} |
74037 | 256 |
if (!stopped) { close2(); close1() } |
52539 | 257 |
|
258 |
true |
|
259 |
} |
|
260 |
} |
|
261 |
||
75393 | 262 |
class Isabelle_Sidekick_Bibtex extends SideKickParser("bibtex") { |
73987
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
263 |
override def supportsCompletion = false |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
264 |
|
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
265 |
private class Asset(label: String, label_html: String, range: Text.Range, source: String) |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
266 |
extends Isabelle_Sidekick.Asset(label, range) { |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
267 |
override def getShortString: String = label_html |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
268 |
override def getLongString: String = source |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
269 |
} |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
270 |
|
75393 | 271 |
def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = { |
73987
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
272 |
val data = Isabelle_Sidekick.root_data(buffer) |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
273 |
|
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
274 |
try { |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
275 |
var offset = 0 |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
276 |
for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
277 |
val kind = chunk.kind |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
278 |
val name = chunk.name |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
279 |
val source = chunk.source |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
280 |
if (kind != "") { |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
281 |
val label = kind + (if (name == "") "" else " " + name) |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
282 |
val label_html = |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
283 |
"<html><b>" + HTML.output(kind) + "</b>" + |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
284 |
(if (name == "") "" else " " + HTML.output(name)) + "</html>" |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
285 |
val range = Text.Range(offset, offset + source.length) |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
286 |
val asset = new Asset(label, label_html, range, source) |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
287 |
data.root.add(new DefaultMutableTreeNode(asset)) |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
288 |
} |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
289 |
offset += source.length |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
290 |
} |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
291 |
data |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
292 |
} |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
293 |
catch { case ERROR(msg) => Output.warning(msg); null } |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
294 |
} |
fc363a3b690a
build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents:
73367
diff
changeset
|
295 |
} |