author | wenzelm |
Sat, 13 Jul 2013 13:25:42 +0200 | |
changeset 52643 | 34c29356930e |
parent 51614 | 22d1dd43f089 |
child 53316 | c3e549e0d3c7 |
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 |
|
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
14 |
import scala.swing.event.ValueChanged |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
15 |
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
|
16 |
|
50299 | 17 |
import org.gjt.sp.jedit.View |
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 |
{ |
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) |
50299 | 24 |
yield (sym, Library.lowercase(sym)) |
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) |
50206 | 29 |
private val font_size = Rendering.font_size("jedit_font_scale").round |
50191
8b5a256859af
more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
wenzelm
parents:
50190
diff
changeset
|
30 |
|
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
31 |
font = |
50191
8b5a256859af
more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
wenzelm
parents:
50190
diff
changeset
|
32 |
Symbol.fonts.get(symbol) match { |
51614
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
50299
diff
changeset
|
33 |
case None => Isabelle_Font(size = font_size) |
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
50299
diff
changeset
|
34 |
case Some(font_family) => Isabelle_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
|
35 |
} |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
36 |
action = |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
37 |
Action(decoded) { |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
38 |
val text_area = view.getTextArea |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
39 |
if (Token_Markup.is_control_style(decoded)) |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
40 |
Token_Markup.edit_control_style(text_area, decoded) |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
41 |
else text_area.setSelectedText(decoded) |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
42 |
text_area.requestFocus |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
43 |
} |
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
|
44 |
tooltip = |
50186
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50185
diff
changeset
|
45 |
JEdit_Lib.wrap_tooltip( |
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50185
diff
changeset
|
46 |
symbol + |
f83cab68c788
recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents:
50185
diff
changeset
|
47 |
(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
|
48 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
49 |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
50 |
private class Reset_Component extends Button |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
51 |
{ |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
52 |
action = Action("Reset") { |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
53 |
val text_area = view.getTextArea |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
54 |
Token_Markup.edit_control_style(text_area, "") |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
55 |
text_area.requestFocus |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
56 |
} |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
57 |
tooltip = "Reset control symbols within text" |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
58 |
} |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
59 |
|
50153 | 60 |
val group_tabs: TabbedPane = new TabbedPane { |
50192 | 61 |
pages ++= |
62 |
Symbol.groups map { case (group, symbols) => |
|
50151 | 63 |
new TabbedPane.Page(group, |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
64 |
new FlowPanel { |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
65 |
contents ++= symbols.map(new Symbol_Component(_)) |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
66 |
if (group == "control") contents += new Reset_Component |
50189 | 67 |
}, null) |
50192 | 68 |
} |
50151 | 69 |
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
|
70 |
val search = new TextField(10) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
71 |
val results_panel = new FlowPanel |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
72 |
add(search, BorderPanel.Position.North) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
73 |
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
|
74 |
listenTo(search) |
50153 | 75 |
val delay_search = |
50207 | 76 |
Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { |
50205 | 77 |
val max_results = PIDE.options.int("jedit_symbols_search_limit") max 0 |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
78 |
results_panel.contents.clear |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
79 |
val results = |
50299 | 80 |
(searchspace filter |
81 |
(Library.lowercase(search.text).split("\\s+") forall _._2.contains) |
|
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
82 |
take (max_results + 1)).toList |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
83 |
for ((sym, _) <- results) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
84 |
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
|
85 |
if (results.length > max_results) results_panel.contents += new Label("...") |
50153 | 86 |
revalidate |
87 |
repaint |
|
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
88 |
} |
50153 | 89 |
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
|
90 |
}, "Search Symbols") |
50151 | 91 |
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
|
92 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
93 |
set_content(group_tabs) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
94 |
} |