author | wenzelm |
Sat, 24 Nov 2012 17:05:10 +0100 | |
changeset 50189 | 5ab700fd5128 |
parent 50187 | b5a09812abc4 |
child 50190 | 0d7f0d8fd63b |
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 |
|
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
12 |
import java.awt.Font |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
13 |
import org.gjt.sp.jedit.View |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
14 |
|
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
15 |
import scala.swing.event.ValueChanged |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
16 |
import scala.swing.{Action, Button, FlowPanel, TabbedPane, TextField, BorderPanel, Label} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
17 |
|
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 |
{ |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
20 |
private val max_results = 50 |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
21 |
|
50145
88ba14e563d4
accomodate scala-2.10.0-RC2 with its slight reform on for-syntax;
wenzelm
parents:
50143
diff
changeset
|
22 |
val searchspace = |
88ba14e563d4
accomodate scala-2.10.0-RC2 with its slight reform on for-syntax;
wenzelm
parents:
50143
diff
changeset
|
23 |
for ((group, symbols) <- Symbol.groups; sym <- symbols) |
50185
820673500454
avoid showing semantic aspects of Unicode -- Isabelle/Scala merely (ab)uses the low-level rendering model (codepoint + font);
wenzelm
parents:
50155
diff
changeset
|
24 |
yield (sym, sym.toLowerCase) |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
25 |
|
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
26 |
private class Symbol_Component(val symbol: String) extends Button |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
27 |
{ |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
28 |
private val decoded = Symbol.decode(symbol) |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
29 |
font = |
50152 | 30 |
new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()), |
50146 | 31 |
Font.PLAIN, Isabelle.font_size("jedit_font_scale").round) |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
32 |
action = |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
33 |
Action(decoded) { |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
34 |
val text_area = view.getTextArea |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
35 |
if (Token_Markup.is_control_style(decoded)) |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
36 |
Token_Markup.edit_control_style(text_area, decoded) |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
37 |
else text_area.setSelectedText(decoded) |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
38 |
text_area.requestFocus |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
39 |
} |
50185
820673500454
avoid showing semantic aspects of Unicode -- Isabelle/Scala merely (ab)uses the low-level rendering model (codepoint + font);
wenzelm
parents:
50155
diff
changeset
|
40 |
tooltip = |
50186
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50185
diff
changeset
|
41 |
JEdit_Lib.wrap_tooltip( |
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50185
diff
changeset
|
42 |
symbol + |
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50185
diff
changeset
|
43 |
(if (Symbol.abbrevs.isDefinedAt(symbol)) "\nabbrev: " + Symbol.abbrevs(symbol) else "")) |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
44 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
45 |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
46 |
private class Reset_Component extends Button |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
47 |
{ |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
48 |
action = Action("Reset") { |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
49 |
val text_area = view.getTextArea |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
50 |
Token_Markup.edit_control_style(text_area, "") |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
51 |
text_area.requestFocus |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
52 |
} |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
53 |
tooltip = "Reset control symbols within text" |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
54 |
} |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
55 |
|
50153 | 56 |
val group_tabs: TabbedPane = new TabbedPane { |
50145
88ba14e563d4
accomodate scala-2.10.0-RC2 with its slight reform on for-syntax;
wenzelm
parents:
50143
diff
changeset
|
57 |
pages ++= (for ((group, symbols) <- Symbol.groups) yield |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
58 |
{ |
50151 | 59 |
new TabbedPane.Page(group, |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
60 |
new FlowPanel { |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
61 |
contents ++= symbols.map(new Symbol_Component(_)) |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
62 |
if (group == "control") contents += new Reset_Component |
50189 | 63 |
}, null) |
50151 | 64 |
}).toList.sortWith(_.title <= _.title) |
65 |
pages += new TabbedPane.Page("search", new BorderPanel { |
|
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
66 |
val search = new TextField(10) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
67 |
val results_panel = new FlowPanel |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
68 |
add(search, BorderPanel.Position.North) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
69 |
add(results_panel, BorderPanel.Position.Center) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
70 |
listenTo(search) |
50153 | 71 |
val delay_search = |
72 |
Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) { |
|
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
73 |
results_panel.contents.clear |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
74 |
val results = |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
75 |
(searchspace filter (search.text.toLowerCase.split("\\s+") forall _._2.contains) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
76 |
take (max_results + 1)).toList |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
77 |
for ((sym, _) <- results) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
78 |
results_panel.contents += new Symbol_Component(sym) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
79 |
if (results.length > max_results) results_panel.contents += new Label("...") |
50153 | 80 |
revalidate |
81 |
repaint |
|
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
82 |
} |
50153 | 83 |
reactions += { case ValueChanged(`search`) => delay_search.invoke() } |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
84 |
}, "Search Symbols") |
50151 | 85 |
pages map (p => p.title = (space_explode('_', p.title) map Library.capitalize).mkString(" ") ) |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
86 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
87 |
set_content(group_tabs) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
88 |
} |