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