author | wenzelm |
Mon, 04 Dec 2017 22:52:16 +0100 | |
changeset 67130 | b023f64e0d16 |
parent 66591 | 6efa351190d0 |
child 67389 | 7e21d19e7ad7 |
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._ |
66591
6efa351190d0
more robust: provide docking framework via base plugin;
wenzelm
parents:
66206
diff
changeset
|
11 |
import isabelle.jedit_base.Dockable |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
12 |
|
56755 | 13 |
import scala.swing.event.{SelectionChanged, ValueChanged} |
63874 | 14 |
import scala.swing.{Component, Action, Button, TabbedPane, TextField, BorderPanel, |
15 |
Label, ScrollPane} |
|
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
16 |
|
63872 | 17 |
import org.gjt.sp.jedit.{EditBus, EBComponent, EBMessage, View} |
50299 | 18 |
|
19 |
||
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
20 |
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
|
21 |
{ |
63870 | 22 |
private def font_size: Int = |
23 |
Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round |
|
24 |
||
63872 | 25 |
|
63877 | 26 |
/* abbrevs */ |
63872 | 27 |
|
28 |
private val abbrevs_panel = new Abbrevs_Panel |
|
29 |
||
30 |
private val abbrevs_refresh_delay = |
|
31 |
GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh } |
|
32 |
||
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
33 |
private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button |
63870 | 34 |
{ |
63874 | 35 |
def update_font { font = GUI.font(size = font_size) } |
36 |
update_font |
|
37 |
||
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
38 |
text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>" |
63870 | 39 |
action = |
40 |
Action(text) { |
|
41 |
val text_area = view.getTextArea |
|
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
42 |
val (s1, s2) = |
67130 | 43 |
Completion.split_template(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, txt)) |
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
44 |
text_area.setSelectedText(s1 + s2) |
63870 | 45 |
text_area.moveCaretPosition(text_area.getCaretPosition - s2.length) |
46 |
text_area.requestFocus |
|
47 |
} |
|
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
48 |
tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a))) |
63870 | 49 |
} |
50 |
||
66206 | 51 |
private class Abbrevs_Panel extends Wrap_Panel(Nil, Wrap_Panel.Alignment.Center) |
63870 | 52 |
{ |
53 |
private var abbrevs: Thy_Header.Abbrevs = Nil |
|
54 |
||
63872 | 55 |
def refresh: Unit = GUI_Thread.require { |
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
56 |
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
|
57 |
|
63870 | 58 |
if (abbrevs != abbrevs1) { |
59 |
abbrevs = abbrevs1 |
|
60 |
||
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
61 |
val entries: List[(String, List[String])] = |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
62 |
Multi_Map( |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
63 |
(for { |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
64 |
(abbr, txt0) <- abbrevs |
63926 | 65 |
txt = Symbol.encode(txt0) |
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
66 |
if !Symbol.iterator(txt). |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
67 |
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
|
68 |
} yield (txt, abbr)): _*).iterator_list.toList |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
69 |
|
63870 | 70 |
contents.clear |
63873
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
71 |
for ((txt, abbrs) <- entries.sortBy(_._1)) |
228a85f1d6af
clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents:
63872
diff
changeset
|
72 |
contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted) |
63870 | 73 |
|
74 |
revalidate |
|
75 |
repaint |
|
76 |
} |
|
77 |
} |
|
63872 | 78 |
|
63870 | 79 |
refresh |
80 |
} |
|
81 |
||
63872 | 82 |
|
83 |
/* symbols */ |
|
84 |
||
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
85 |
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
|
86 |
{ |
63874 | 87 |
def update_font |
88 |
{ |
|
89 |
font = |
|
90 |
Symbol.fonts.get(symbol) match { |
|
91 |
case None => GUI.font(size = font_size) |
|
92 |
case Some(font_family) => GUI.font(family = font_family, size = font_size) |
|
93 |
} |
|
94 |
} |
|
95 |
update_font |
|
96 |
||
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
97 |
action = |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
98 |
Action(Symbol.decode(symbol)) { |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
99 |
val text_area = view.getTextArea |
65997
e3dc9ea67a62
output control symbols like ML version, with optionally hidden source;
wenzelm
parents:
65259
diff
changeset
|
100 |
if (is_control && HTML.is_control(symbol)) |
65259 | 101 |
Syntax_Style.edit_control_style(text_area, symbol) |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
102 |
else |
67130 | 103 |
text_area.setSelectedText(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, symbol)) |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
104 |
text_area.requestFocus |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
105 |
} |
56622
891d1b8b64fb
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents:
56609
diff
changeset
|
106 |
tooltip = |
891d1b8b64fb
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents:
56609
diff
changeset
|
107 |
GUI.tooltip_lines( |
891d1b8b64fb
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents:
56609
diff
changeset
|
108 |
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
|
109 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
110 |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
111 |
private class Reset_Component extends Button |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
112 |
{ |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
113 |
action = Action("Reset") { |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
114 |
val text_area = view.getTextArea |
65259 | 115 |
Syntax_Style.edit_control_style(text_area, "") |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
116 |
text_area.requestFocus |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
117 |
} |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
118 |
tooltip = "Reset control symbols within text" |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
119 |
} |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
120 |
|
63872 | 121 |
|
63877 | 122 |
/* search */ |
123 |
||
124 |
private class Search_Panel extends BorderPanel { |
|
125 |
val search_field = new TextField(10) |
|
66206 | 126 |
val results_panel = Wrap_Panel(Nil, Wrap_Panel.Alignment.Center) |
63877 | 127 |
layout(search_field) = BorderPanel.Position.North |
128 |
layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center |
|
129 |
||
130 |
val search_space = |
|
131 |
(for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList |
|
132 |
val search_delay = |
|
133 |
GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { |
|
134 |
val search_words = Word.explode(Word.lowercase(search_field.text)) |
|
135 |
val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0 |
|
136 |
val results = |
|
137 |
for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym |
|
138 |
||
139 |
results_panel.contents.clear |
|
140 |
for (sym <- results.take(search_limit)) |
|
141 |
results_panel.contents += new Symbol_Component(sym, false) |
|
142 |
if (results.length > search_limit) |
|
143 |
results_panel.contents += |
|
144 |
new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" } |
|
145 |
revalidate |
|
146 |
repaint |
|
147 |
} |
|
148 |
search_field.reactions += { case ValueChanged(_) => search_delay.invoke() } |
|
149 |
} |
|
150 |
||
151 |
||
63872 | 152 |
/* tabs */ |
63870 | 153 |
|
56756 | 154 |
private val group_tabs: TabbedPane = new TabbedPane { |
63870 | 155 |
pages += new TabbedPane.Page("abbrevs", abbrevs_panel) |
156 |
||
50192 | 157 |
pages ++= |
56753 | 158 |
Symbol.groups.map({ case (group, symbols) => |
66205 | 159 |
val control = group == "control" |
50151 | 160 |
new TabbedPane.Page(group, |
66205 | 161 |
new ScrollPane(Wrap_Panel( |
162 |
symbols.map(new Symbol_Component(_, control)) ::: |
|
66206 | 163 |
(if (control) List(new Reset_Component) else Nil), |
164 |
Wrap_Panel.Alignment.Center)), null) |
|
56753 | 165 |
}) |
166 |
||
63877 | 167 |
val search_panel = new Search_Panel |
168 |
val search_page = new TabbedPane.Page("search", search_panel, "Search Symbols") |
|
56755 | 169 |
pages += search_page |
170 |
||
171 |
listenTo(selection) |
|
172 |
reactions += { |
|
63877 | 173 |
case SelectionChanged(_) if selection.page == search_page => |
174 |
search_panel.search_field.requestFocus |
|
56755 | 175 |
} |
176 |
||
56756 | 177 |
for (page <- pages) |
178 |
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
|
179 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
180 |
set_content(group_tabs) |
63872 | 181 |
|
182 |
||
183 |
||
184 |
/* main */ |
|
185 |
||
186 |
private val edit_bus_handler: EBComponent = |
|
187 |
new EBComponent { def handleMessage(msg: EBMessage) { abbrevs_refresh_delay.invoke() } } |
|
188 |
||
189 |
private val main = |
|
190 |
Session.Consumer[Any](getClass.getName) { |
|
63874 | 191 |
case _: Session.Global_Options => |
192 |
GUI_Thread.later { |
|
193 |
val comp = group_tabs.peer |
|
194 |
GUI.traverse_components(comp, |
|
195 |
{ |
|
196 |
case c0: javax.swing.JComponent => |
|
197 |
Component.wrap(c0) match { |
|
198 |
case c: Abbrev_Component => c.update_font |
|
199 |
case c: Symbol_Component => c.update_font |
|
200 |
case _ => |
|
201 |
} |
|
202 |
case _ => |
|
203 |
}) |
|
204 |
comp.revalidate |
|
205 |
comp.repaint() |
|
206 |
} |
|
63872 | 207 |
case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke() |
208 |
} |
|
209 |
||
210 |
override def init() |
|
211 |
{ |
|
212 |
EditBus.addToBus(edit_bus_handler) |
|
63874 | 213 |
PIDE.session.global_options += main |
63872 | 214 |
PIDE.session.commands_changed += main |
215 |
} |
|
216 |
||
217 |
override def exit() |
|
218 |
{ |
|
219 |
EditBus.removeFromBus(edit_bus_handler) |
|
63874 | 220 |
PIDE.session.global_options -= main |
63872 | 221 |
PIDE.session.commands_changed -= main |
222 |
} |
|
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
223 |
} |