author | immler |
Wed, 21 Nov 2012 16:21:16 +0100 | |
changeset 50154 | ab5272955b3b |
parent 50153 | e6121a825db8 |
child 50155 | e2c08f20d00e |
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) |
88ba14e563d4
accomodate scala-2.10.0-RC2 with its slight reform on for-syntax;
wenzelm
parents:
50143
diff
changeset
|
24 |
yield (sym, (sym.toLowerCase + get_name(Symbol.decode(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 |
def get_name(c: String): String = |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
27 |
if (c.length >= 1) Character.getName(c.codePointAt(0)) else "??" |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
28 |
|
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
29 |
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
|
30 |
{ |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
31 |
val dec = Symbol.decode(symbol) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
32 |
font = |
50152 | 33 |
new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()), |
50146 | 34 |
Font.PLAIN, Isabelle.font_size("jedit_font_scale").round) |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
35 |
action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus } |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
36 |
tooltip = symbol + " - " + get_name(dec) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
37 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
38 |
|
50153 | 39 |
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
|
40 |
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
|
41 |
{ |
50151 | 42 |
new TabbedPane.Page(group, |
50154
ab5272955b3b
removed (unicode) tooltips: can not adjust font in basic swing tooltip
immler
parents:
50153
diff
changeset
|
43 |
new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) }) |
50151 | 44 |
}).toList.sortWith(_.title <= _.title) |
45 |
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
|
46 |
val search = new TextField(10) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
47 |
val results_panel = new FlowPanel |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
48 |
add(search, BorderPanel.Position.North) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
49 |
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
|
50 |
listenTo(search) |
50153 | 51 |
val delay_search = |
52 |
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
|
53 |
results_panel.contents.clear |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
54 |
val results = |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
55 |
(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
|
56 |
take (max_results + 1)).toList |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
57 |
for ((sym, _) <- results) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
58 |
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
|
59 |
if (results.length > max_results) results_panel.contents += new Label("...") |
50153 | 60 |
revalidate |
61 |
repaint |
|
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
62 |
} |
50153 | 63 |
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
|
64 |
}, "Search Symbols") |
50151 | 65 |
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
|
66 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
67 |
set_content(group_tabs) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
68 |
} |