author | wenzelm |
Sat, 04 Oct 2014 12:19:26 +0200 | |
changeset 58529 | cd4439d8799c |
parent 58526 | f05ccce3eca2 |
child 58530 | 7ee248f19ca9 |
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 |
|
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 |
||
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 |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
15 |
import javax.swing.Icon |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
16 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
17 |
import org.gjt.sp.jedit.Buffer |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
18 |
import sidekick.{SideKickParser, SideKickParsedData, IAsset} |
34701
80b0add08eef
IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents:
34669
diff
changeset
|
19 |
|
34393 | 20 |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
21 |
object Isabelle_Sidekick |
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
22 |
{ |
40477 | 23 |
def int_to_pos(offset: Text.Offset): Position = |
57912 | 24 |
new Position { def getOffset = offset; override def toString: String = offset.toString } |
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
|
25 |
|
58526 | 26 |
def root_data(buffer: Buffer): SideKickParsedData = |
27 |
{ |
|
28 |
val data = new SideKickParsedData(buffer.getName) |
|
29 |
data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength)) |
|
30 |
data |
|
31 |
} |
|
32 |
||
40477 | 33 |
class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset |
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
|
34 |
{ |
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
|
35 |
protected var _name = 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
|
36 |
protected var _start = int_to_pos(start) |
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
|
37 |
protected var _end = int_to_pos(end) |
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
|
38 |
override def getIcon: Icon = null |
53973
78bbe75c8437
enforce IsabelleText font for better symbol coverage, especially on Windows;
wenzelm
parents:
53281
diff
changeset
|
39 |
override def getShortString: String = |
55825 | 40 |
"<html><span style=\"font-family: " + Font_Info.main_family() + ";\">" + |
53985 | 41 |
HTML.encode(_name) + "</span></html>" |
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
|
42 |
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
|
43 |
override def getName: 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
|
44 |
override def setName(name: String) = _name = 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
|
45 |
override def getStart: Position = _start |
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
|
46 |
override def setStart(start: Position) = _start = start |
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
|
47 |
override def getEnd: Position = _end |
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
|
48 |
override def setEnd(end: Position) = _end = end |
57912 | 49 |
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
|
50 |
} |
51618
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
51 |
|
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
52 |
def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode, |
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
53 |
swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode) |
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
54 |
{ |
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
55 |
for ((_, entry) <- tree.branches) { |
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
56 |
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
|
57 |
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
|
58 |
parent.add(node) |
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
59 |
} |
a3577cd80c41
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents:
51493
diff
changeset
|
60 |
} |
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
61 |
} |
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
62 |
|
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
63 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
64 |
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
|
65 |
{ |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
66 |
override def supportsCompletion = false |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
67 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
68 |
|
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
69 |
/* parsing */ |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
70 |
|
36759 | 71 |
@volatile protected var stopped = false |
34503 | 72 |
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
|
73 |
|
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
74 |
def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false |
36759 | 75 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
76 |
def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = |
34625
799a40faa4f1
completion: decode symbols only if isabelle encoding is active (to prevent unicode chars written back to file);
wenzelm
parents:
34612
diff
changeset
|
77 |
{ |
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
78 |
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
|
79 |
|
38640 | 80 |
// FIXME lock buffer (!??) |
58526 | 81 |
val data = Isabelle_Sidekick.root_data(buffer) |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
82 |
val syntax = Isabelle.mode_syntax(name) |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
83 |
val ok = |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
84 |
if (syntax.isDefined) { |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
85 |
val ok = parser(buffer, syntax.get, data) |
58526 | 86 |
if (stopped) { data.root.add(new DefaultMutableTreeNode("<stopped>")); true } |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
87 |
else ok |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
88 |
} |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
89 |
else false |
58526 | 90 |
if (!ok) data.root.add(new DefaultMutableTreeNode("<ignored>")) |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
91 |
|
34417
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
92 |
data |
bce2f2ea9819
misc tuning and adaption according to original IsabelleParser --
wenzelm
parents:
34408
diff
changeset
|
93 |
} |
34393 | 94 |
} |
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
95 |
|
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
96 |
|
48718 | 97 |
class Isabelle_Sidekick_Structure( |
98 |
name: String, |
|
99 |
node_name: Buffer => Option[Document.Node.Name]) |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
100 |
extends Isabelle_Sidekick(name) |
36759 | 101 |
{ |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
102 |
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = |
36759 | 103 |
{ |
57900 | 104 |
def make_tree(offset: Text.Offset, entry: Thy_Structure.Entry): List[DefaultMutableTreeNode] = |
40455
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
105 |
entry match { |
57900 | 106 |
case Thy_Structure.Block(name, body) => |
40455
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
107 |
val node = |
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
108 |
new DefaultMutableTreeNode( |
40475 | 109 |
new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length)) |
40455
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
110 |
(offset /: body)((i, e) => |
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
111 |
{ |
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
112 |
make_tree(i, e) foreach (nd => node.add(nd)) |
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
113 |
i + e.length |
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
114 |
}) |
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
115 |
List(node) |
57900 | 116 |
case Thy_Structure.Atom(command) |
57904 | 117 |
if command.is_proper && syntax.heading_level(command).isEmpty => |
40455
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
118 |
val node = |
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
119 |
new DefaultMutableTreeNode( |
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
120 |
new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length)) |
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
121 |
List(node) |
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
122 |
case _ => Nil |
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
123 |
} |
e035dad8eca2
default Sidekick parser based on section headings;
wenzelm
parents:
40452
diff
changeset
|
124 |
|
48718 | 125 |
node_name(buffer) match { |
126 |
case Some(name) => |
|
49406 | 127 |
val text = JEdit_Lib.buffer_text(buffer) |
57900 | 128 |
val structure = Thy_Structure.parse(syntax, name, text) |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
129 |
make_tree(0, structure) foreach (node => data.root.add(node)) |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
130 |
true |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
131 |
case None => false |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
132 |
} |
36759 | 133 |
} |
134 |
} |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
135 |
|
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
136 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
137 |
class Isabelle_Sidekick_Default extends |
56208 | 138 |
Isabelle_Sidekick_Structure("isabelle", PIDE.resources.theory_node_name) |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
139 |
|
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
140 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
141 |
class Isabelle_Sidekick_Options extends |
54515 | 142 |
Isabelle_Sidekick_Structure("isabelle-options", _ => Some(Document.Node.Name("options"))) |
48718 | 143 |
|
144 |
||
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
145 |
class Isabelle_Sidekick_Root extends |
54515 | 146 |
Isabelle_Sidekick_Structure("isabelle-root", _ => Some(Document.Node.Name("ROOT"))) |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
147 |
|
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
148 |
|
53281
251e1a2aa792
clarified SideKick parser name, which serves as quasi "mode" here;
wenzelm
parents:
53274
diff
changeset
|
149 |
class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup") |
36759 | 150 |
{ |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
151 |
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = |
36759 | 152 |
{ |
55513
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
153 |
val opt_snapshot = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56814
diff
changeset
|
154 |
GUI_Thread.now { |
55513
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
155 |
Document_Model(buffer) match { |
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
156 |
case Some(model) if model.is_theory => Some(model.snapshot) |
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
157 |
case _ => None |
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
158 |
} |
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
159 |
} |
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
160 |
opt_snapshot match { |
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
161 |
case Some(snapshot) => |
56373
0605d90be6fc
tuned signature -- more explicit iterator terminology;
wenzelm
parents:
56301
diff
changeset
|
162 |
for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) { |
55650 | 163 |
val markup = |
56301
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56299
diff
changeset
|
164 |
snapshot.state.command_markup( |
1da7b4c33db9
more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents:
56299
diff
changeset
|
165 |
snapshot.version, command, Command.Markup_Index.markup, |
56743 | 166 |
command.range, Markup.Elements.full) |
58526 | 167 |
Isabelle_Sidekick.swing_markup_tree(markup, data.root, |
168 |
(info: Text.Info[List[XML.Elem]]) => |
|
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
169 |
{ |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
170 |
val range = info.range + command_start |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
171 |
val content = command.source(info.range).replace('\n', ' ') |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
172 |
val info_text = |
51493
59d8a1031c00
allow fractional pretty margin -- avoid premature rounding;
wenzelm
parents:
50725
diff
changeset
|
173 |
Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0) |
59d8a1031c00
allow fractional pretty margin -- avoid premature rounding;
wenzelm
parents:
50725
diff
changeset
|
174 |
.mkString |
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
175 |
|
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
176 |
new DefaultMutableTreeNode( |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
177 |
new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) { |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
178 |
override def getShortString: String = content |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
179 |
override def getLongString: String = info_text |
57912 | 180 |
override def toString: String = quote(content) + " " + range.toString |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
181 |
}) |
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
|
182 |
}) |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
183 |
} |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
47749
diff
changeset
|
184 |
true |
55513
6d21415e3909
recovered Isabelle_Sidekick_Markup from 9c53198dbb1c: snapshot requires Swing_Thread;
wenzelm
parents:
55432
diff
changeset
|
185 |
case None => false |
36759 | 186 |
} |
187 |
} |
|
188 |
} |
|
36738
dce592144219
support several sidekick parsers -- very basic default parser;
wenzelm
parents:
36737
diff
changeset
|
189 |
|
52539 | 190 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
191 |
class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news") |
52539 | 192 |
{ |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
193 |
private val Heading1 = """^New in (.*)\w*$""".r |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53233
diff
changeset
|
194 |
private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r |
52539 | 195 |
|
196 |
private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode = |
|
197 |
new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, start, stop)) |
|
198 |
||
199 |
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = |
|
200 |
{ |
|
201 |
var offset = 0 |
|
202 |
||
203 |
for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) { |
|
204 |
line match { |
|
205 |
case Heading1(s) => |
|
56814 | 206 |
data.root.add(make_node(s, offset, offset + line.length)) |
52539 | 207 |
case Heading2(s) => |
208 |
data.root.getLastChild.asInstanceOf[DefaultMutableTreeNode] |
|
209 |
.add(make_node(s, offset, offset + line.length)) |
|
210 |
case _ => |
|
211 |
} |
|
212 |
offset += line.length + 1 |
|
213 |
} |
|
214 |
||
215 |
true |
|
216 |
} |
|
217 |
} |
|
218 |
||
58526 | 219 |
|
220 |
class Isabelle_Sidekick_Bibtex extends SideKickParser("bibtex") |
|
221 |
{ |
|
222 |
override def supportsCompletion = false |
|
223 |
||
224 |
private class Asset(label: String, start: Text.Offset, stop: Text.Offset) extends |
|
225 |
Isabelle_Sidekick.Asset(label, start, stop) { override def getShortString: String = _name } |
|
226 |
||
227 |
def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = |
|
228 |
{ |
|
229 |
val data = Isabelle_Sidekick.root_data(buffer) |
|
230 |
||
231 |
try { |
|
232 |
var offset = 0 |
|
233 |
for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { |
|
58529 | 234 |
val n = chunk.source.size |
58526 | 235 |
chunk match { |
236 |
case item: Bibtex.Item if item.is_wellformed => |
|
237 |
val label = if (item.name == "") item.kind else item.kind + " " + item.name |
|
238 |
val asset = new Isabelle_Sidekick.Asset(label, offset, offset + n) |
|
239 |
data.root.add(new DefaultMutableTreeNode(asset)) |
|
240 |
case _ => |
|
241 |
} |
|
242 |
offset += n |
|
243 |
} |
|
244 |
data |
|
245 |
} |
|
246 |
catch { case ERROR(_) => null } |
|
247 |
} |
|
248 |
} |
|
249 |