author | wenzelm |
Wed, 14 Sep 2016 14:17:32 +0200 | |
changeset 63870 | 6db1aac936db |
parent 62104 | fb73c0d7bb37 |
child 63872 | 7dd5297d87fa |
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 |
|
50299 | 15 |
import org.gjt.sp.jedit.View |
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 |
||
23 |
private class Abbrev_Component(val abbrev: (String, String)) extends Button |
|
24 |
{ |
|
25 |
text = Symbol.decode(abbrev._2) |
|
26 |
font = GUI.font(size = font_size) |
|
27 |
action = |
|
28 |
Action(text) { |
|
29 |
val text_area = view.getTextArea |
|
30 |
val (s1, s2) = Completion.split_template(text) |
|
31 |
text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, s1 + s2)) |
|
32 |
text_area.moveCaretPosition(text_area.getCaretPosition - s2.length) |
|
33 |
text_area.requestFocus |
|
34 |
} |
|
35 |
tooltip = |
|
36 |
GUI.tooltip_lines(cat_lines(List(abbrev._2, "abbrev: " + abbrev._1))) |
|
37 |
} |
|
38 |
||
39 |
private class Abbrevs_Panel extends Wrap_Panel |
|
40 |
{ |
|
41 |
private var abbrevs: Thy_Header.Abbrevs = Nil |
|
42 |
||
43 |
def refresh |
|
44 |
{ |
|
45 |
val abbrevs1 = |
|
46 |
Isabelle.buffer_syntax(view.getBuffer).getOrElse(Outer_Syntax.empty).abbrevs |
|
47 |
if (abbrevs != abbrevs1) { |
|
48 |
abbrevs = abbrevs1 |
|
49 |
||
50 |
contents.clear |
|
51 |
for { |
|
52 |
abbrev <- abbrevs |
|
53 |
if !Symbol.iterator(Symbol.encode(abbrev._2)). |
|
54 |
forall(s => s.length == 1 && s(0) != Completion.caret_indicator) |
|
55 |
} { contents += new Abbrev_Component(abbrev) } |
|
56 |
||
57 |
revalidate |
|
58 |
repaint |
|
59 |
} |
|
60 |
} |
|
61 |
refresh |
|
62 |
} |
|
63 |
||
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
64 |
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
|
65 |
{ |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
66 |
font = |
50191
8b5a256859af
more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
wenzelm
parents:
50190
diff
changeset
|
67 |
Symbol.fonts.get(symbol) match { |
57908
1937603dbdf2
separate Java FX modules -- no need to include jfxrt.jar by default;
wenzelm
parents:
57612
diff
changeset
|
68 |
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
|
69 |
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
|
70 |
} |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
71 |
action = |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
72 |
Action(Symbol.decode(symbol)) { |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
73 |
val text_area = view.getTextArea |
62104
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
74 |
if (is_control && HTML.control.isDefinedAt(symbol)) |
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
75 |
Token_Markup.edit_control_style(text_area, symbol) |
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
76 |
else |
fb73c0d7bb37
clarified symbol insertion, depending on buffer encoding;
wenzelm
parents:
62024
diff
changeset
|
77 |
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
|
78 |
text_area.requestFocus |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
79 |
} |
56622
891d1b8b64fb
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents:
56609
diff
changeset
|
80 |
tooltip = |
891d1b8b64fb
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents:
56609
diff
changeset
|
81 |
GUI.tooltip_lines( |
891d1b8b64fb
clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents:
56609
diff
changeset
|
82 |
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
|
83 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
84 |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
85 |
private class Reset_Component extends Button |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
86 |
{ |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
87 |
action = Action("Reset") { |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
88 |
val text_area = view.getTextArea |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
89 |
Token_Markup.edit_control_style(text_area, "") |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
90 |
text_area.requestFocus |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
91 |
} |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
92 |
tooltip = "Reset control symbols within text" |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
93 |
} |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
94 |
|
63870 | 95 |
private val abbrevs_panel = new Abbrevs_Panel |
96 |
||
56756 | 97 |
private val group_tabs: TabbedPane = new TabbedPane { |
63870 | 98 |
pages += new TabbedPane.Page("abbrevs", abbrevs_panel) |
99 |
||
50192 | 100 |
pages ++= |
56753 | 101 |
Symbol.groups.map({ case (group, symbols) => |
50151 | 102 |
new TabbedPane.Page(group, |
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53316
diff
changeset
|
103 |
new ScrollPane(new Wrap_Panel { |
62024
e3e22a5e85f2
clarified meaning of \<^bold> action, depending on group;
wenzelm
parents:
59391
diff
changeset
|
104 |
val control = group == "control" |
e3e22a5e85f2
clarified meaning of \<^bold> action, depending on group;
wenzelm
parents:
59391
diff
changeset
|
105 |
contents ++= symbols.map(new Symbol_Component(_, control)) |
e3e22a5e85f2
clarified meaning of \<^bold> action, depending on group;
wenzelm
parents:
59391
diff
changeset
|
106 |
if (control) contents += new Reset_Component |
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53316
diff
changeset
|
107 |
}), null) |
56753 | 108 |
}) |
109 |
||
56755 | 110 |
val search_field = new TextField(10) |
111 |
val search_page = |
|
112 |
new TabbedPane.Page("search", new BorderPanel { |
|
113 |
val results_panel = new Wrap_Panel |
|
59391 | 114 |
layout(search_field) = BorderPanel.Position.North |
115 |
layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center |
|
56755 | 116 |
|
117 |
val search_space = |
|
118 |
(for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList |
|
56769 | 119 |
val search_delay = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
56769
diff
changeset
|
120 |
GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { |
56756 | 121 |
val search_words = Word.explode(Word.lowercase(search_field.text)) |
56755 | 122 |
val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0 |
56756 | 123 |
val results = |
124 |
for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym |
|
125 |
||
56755 | 126 |
results_panel.contents.clear |
127 |
for (sym <- results.take(search_limit)) |
|
62024
e3e22a5e85f2
clarified meaning of \<^bold> action, depending on group;
wenzelm
parents:
59391
diff
changeset
|
128 |
results_panel.contents += new Symbol_Component(sym, false) |
56755 | 129 |
if (results.length > search_limit) |
56756 | 130 |
results_panel.contents += |
131 |
new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" } |
|
56755 | 132 |
revalidate |
133 |
repaint |
|
134 |
} |
|
56769 | 135 |
search_field.reactions += { case ValueChanged(_) => search_delay.invoke() } |
56755 | 136 |
}, "Search Symbols") |
137 |
pages += search_page |
|
138 |
||
139 |
listenTo(selection) |
|
140 |
reactions += { |
|
141 |
case SelectionChanged(_) if selection.page == search_page => search_field.requestFocus |
|
142 |
} |
|
143 |
||
56756 | 144 |
for (page <- pages) |
145 |
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
|
146 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
147 |
set_content(group_tabs) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
148 |
} |