author | wenzelm |
Wed, 14 Sep 2016 19:44:08 +0200 | |
changeset 63873 | 228a85f1d6af |
parent 63872 | 7dd5297d87fa |
child 63874 | e2393cfde472 |
permissions | -rw-r--r-- |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/symbols_dockable.scala |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
2 |
Author: Fabian Immler |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
3 |
|
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
4 |
Dockable window for Symbol Palette. |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
5 |
*/ |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
6 |
|
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
7 |
package isabelle.jedit |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
8 |
|
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
9 |
|
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
10 |
import isabelle._ |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
11 |
|
56755 | 12 |
import scala.swing.event.{SelectionChanged, ValueChanged} |
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53316
diff
changeset
|
13 |
import scala.swing.{Action, Button, TabbedPane, TextField, BorderPanel, Label, ScrollPane} |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
14 |
|
63872 | 15 |
import org.gjt.sp.jedit.{EditBus, EBComponent, EBMessage, View} |
50299 | 16 |
|
17 |
||
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
18 |
class Symbols_Dockable(view: View, position: String) extends Dockable(view, position) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
19 |
{ |
63870 | 20 |
private def font_size: Int = |
21 |
Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round |
|
22 |
||
63872 | 23 |
|
24 |
/* abbreviations */ |
|
25 |
||
26 |
private val abbrevs_panel = new Abbrevs_Panel |
|
27 |
||
28 |
private val abbrevs_refresh_delay = |
|
29 |
GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh } |
|
30 |
||
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
31 |
private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button |
63870 | 32 |
{ |
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
33 |
text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>" |
63870 | 34 |
font = GUI.font(size = font_size) |
35 |
action = |
|
36 |
Action(text) { |
|
37 |
val text_area = view.getTextArea |
|
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
38 |
val (s1, s2) = |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
39 |
Completion.split_template(Isabelle_Encoding.maybe_decode(text_area.getBuffer, txt)) |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
40 |
text_area.setSelectedText(s1 + s2) |
63870 | 41 |
text_area.moveCaretPosition(text_area.getCaretPosition - s2.length) |
42 |
text_area.requestFocus |
|
43 |
} |
|
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
44 |
tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a))) |
63870 | 45 |
} |
46 |
||
47 |
private class Abbrevs_Panel extends Wrap_Panel |
|
48 |
{ |
|
49 |
private var abbrevs: Thy_Header.Abbrevs = Nil |
|
50 |
||
63872 | 51 |
def refresh: Unit = GUI_Thread.require { |
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
52 |
val abbrevs1 = Isabelle.buffer_syntax(view.getBuffer).getOrElse(Outer_Syntax.empty).abbrevs |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
53 |
|
63870 | 54 |
if (abbrevs != abbrevs1) { |
55 |
abbrevs = abbrevs1 |
|
56 |
||
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
57 |
val entries: List[(String, List[String])] = |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
58 |
Multi_Map( |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
59 |
(for { |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
60 |
(abbr, txt0) <- abbrevs |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
61 |
val txt = Symbol.encode(txt0) |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
62 |
if !Symbol.iterator(txt). |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
63 |
forall(s => s.length == 1 && s(0) != Completion.caret_indicator) |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
64 |
} yield (txt, abbr)): _*).iterator_list.toList |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
65 |
|
63870 | 66 |
contents.clear |
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
67 |
for ((txt, abbrs) <- entries.sortBy(_._1)) |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
68 |
contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted) |
63870 | 69 |
|
70 |
revalidate |
|
71 |
repaint |
|
72 |
} |
|
73 |
} |
|
63872 | 74 |
|
63870 | 75 |
refresh |
76 |
} |
|
77 |
||
63872 | 78 |
|
79 |
/* symbols */ |
|
80 |
||
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
81 |
private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
82 |
{ |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
83 |
font = |
50191
8b5a256859af
more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
wenzelm
parents:
50190
diff
changeset
|
84 |
Symbol.fonts.get(symbol) match { |
57908
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents:
57612
diff
changeset
|
85 |
case None => GUI.font(size = font_size) |
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents:
57612
diff
changeset
|
86 |
case Some(font_family) => GUI.font(family = font_family, size = font_size) |
50191
8b5a256859af
more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
wenzelm
parents:
50190
diff
changeset
|
87 |
} |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
88 |
action = |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
89 |
Action(Symbol.decode(symbol)) { |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
90 |
val text_area = view.getTextArea |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
91 |
if (is_control && HTML.control.isDefinedAt(symbol)) |
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
92 |
Token_Markup.edit_control_style(text_area, symbol) |
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
93 |
else |
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
94 |
text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol)) |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
95 |
text_area.requestFocus |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
96 |
} |
56622
891d1b8b64fb
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents:
56609
diff
changeset
|
97 |
tooltip = |
891d1b8b64fb
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents:
56609
diff
changeset
|
98 |
GUI.tooltip_lines( |
891d1b8b64fb
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents:
56609
diff
changeset
|
99 |
cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a))) |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
100 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
101 |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
102 |
private class Reset_Component extends Button |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
103 |
{ |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
104 |
action = Action("Reset") { |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
105 |
val text_area = view.getTextArea |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
106 |
Token_Markup.edit_control_style(text_area, "") |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
107 |
text_area.requestFocus |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
108 |
} |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
109 |
tooltip = "Reset control symbols within text" |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
110 |
} |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
111 |
|
63872 | 112 |
|
113 |
/* tabs */ |
|
63870 | 114 |
|
56756 | 115 |
private val group_tabs: TabbedPane = new TabbedPane { |
63870 | 116 |
pages += new TabbedPane.Page("abbrevs", abbrevs_panel) |
117 |
||
50192 | 118 |
pages ++= |
56753 | 119 |
Symbol.groups.map({ case (group, symbols) => |
50151 | 120 |
new TabbedPane.Page(group, |
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53316
diff
changeset
|
121 |
new ScrollPane(new Wrap_Panel { |
62024
e3e22a5e85f2
clarified meaning of \<^bold> action, depending on group;
wenzelm
parents:
59391
diff
changeset
|
122 |
val control = group == "control" |
e3e22a5e85f2
clarified meaning of \<^bold> action, depending on group;
wenzelm
parents:
59391
diff
changeset
|
123 |
contents ++= symbols.map(new Symbol_Component(_, control)) |
e3e22a5e85f2
clarified meaning of \<^bold> action, depending on group;
wenzelm
parents:
59391
diff
changeset
|
124 |
if (control) contents += new Reset_Component |
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53316
diff
changeset
|
125 |
}), null) |
56753 | 126 |
}) |
127 |
||
56755 | 128 |
val search_field = new TextField(10) |
129 |
val search_page = |
|
130 |
new TabbedPane.Page("search", new BorderPanel { |
|
131 |
val results_panel = new Wrap_Panel |
|
59391 | 132 |
layout(search_field) = BorderPanel.Position.North |
133 |
layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center |
|
56755 | 134 |
|
135 |
val search_space = |
|
136 |
(for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList |
|
56769 | 137 |
val search_delay = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56769
diff
changeset
|
138 |
GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { |
56756 | 139 |
val search_words = Word.explode(Word.lowercase(search_field.text)) |
56755 | 140 |
val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0 |
56756 | 141 |
val results = |
142 |
for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym |
|
143 |
||
56755 | 144 |
results_panel.contents.clear |
145 |
for (sym <- results.take(search_limit)) |
|
62024
e3e22a5e85f2
clarified meaning of \<^bold> action, depending on group;
wenzelm
parents:
59391
diff
changeset
|
146 |
results_panel.contents += new Symbol_Component(sym, false) |
56755 | 147 |
if (results.length > search_limit) |
56756 | 148 |
results_panel.contents += |
149 |
new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" } |
|
56755 | 150 |
revalidate |
151 |
repaint |
|
152 |
} |
|
56769 | 153 |
search_field.reactions += { case ValueChanged(_) => search_delay.invoke() } |
56755 | 154 |
}, "Search Symbols") |
155 |
pages += search_page |
|
156 |
||
157 |
listenTo(selection) |
|
158 |
reactions += { |
|
159 |
case SelectionChanged(_) if selection.page == search_page => search_field.requestFocus |
|
160 |
} |
|
161 |
||
56756 | 162 |
for (page <- pages) |
163 |
page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_))) |
|
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
164 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
165 |
set_content(group_tabs) |
63872 | 166 |
|
167 |
||
168 |
||
169 |
/* main */ |
|
170 |
||
171 |
private val edit_bus_handler: EBComponent = |
|
172 |
new EBComponent { def handleMessage(msg: EBMessage) { abbrevs_refresh_delay.invoke() } } |
|
173 |
||
174 |
private val main = |
|
175 |
Session.Consumer[Any](getClass.getName) { |
|
176 |
case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke() |
|
177 |
} |
|
178 |
||
179 |
override def init() |
|
180 |
{ |
|
181 |
EditBus.addToBus(edit_bus_handler) |
|
182 |
PIDE.session.commands_changed += main |
|
183 |
} |
|
184 |
||
185 |
override def exit() |
|
186 |
{ |
|
187 |
EditBus.removeFromBus(edit_bus_handler) |
|
188 |
PIDE.session.commands_changed -= main |
|
189 |
} |
|
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
190 |
} |