author | wenzelm |
Thu, 17 Apr 2014 10:54:10 +0200 | |
changeset 56609 | 5ac67041ccf8 |
parent 56600 | 628e039cc34d |
child 56622 | 891d1b8b64fb |
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 |
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53316
diff
changeset
|
15 |
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
|
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) |
56599 | 24 |
yield (sym, Word.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) |
55825 | 29 |
private val font_size = Font_Info.main_size(PIDE.options.real("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 |
} |
53786 | 44 |
tooltip = GUI.tooltip_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
|
45 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
46 |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
47 |
private class Reset_Component extends Button |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
48 |
{ |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
49 |
action = Action("Reset") { |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
50 |
val text_area = view.getTextArea |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
51 |
Token_Markup.edit_control_style(text_area, "") |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
52 |
text_area.requestFocus |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
53 |
} |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
54 |
tooltip = "Reset control symbols within text" |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
55 |
} |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
56 |
|
50153 | 57 |
val group_tabs: TabbedPane = new TabbedPane { |
50192 | 58 |
pages ++= |
59 |
Symbol.groups map { case (group, symbols) => |
|
50151 | 60 |
new TabbedPane.Page(group, |
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53316
diff
changeset
|
61 |
new ScrollPane(new Wrap_Panel { |
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
62 |
contents ++= symbols.map(new Symbol_Component(_)) |
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50186
diff
changeset
|
63 |
if (group == "control") contents += new Reset_Component |
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53316
diff
changeset
|
64 |
}), null) |
50192 | 65 |
} |
50151 | 66 |
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
|
67 |
val search = new TextField(10) |
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53316
diff
changeset
|
68 |
val results_panel = new Wrap_Panel |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
69 |
add(search, BorderPanel.Position.North) |
53713
bb15972a644d
improved layout, with special treatment for ScrollPane;
wenzelm
parents:
53316
diff
changeset
|
70 |
add(new ScrollPane(results_panel), BorderPanel.Position.Center) |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
71 |
listenTo(search) |
50153 | 72 |
val delay_search = |
50207 | 73 |
Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { |
50205 | 74 |
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
|
75 |
results_panel.contents.clear |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
76 |
val results = |
50299 | 77 |
(searchspace filter |
56600 | 78 |
(Word.explode(Word.lowercase(search.text)) forall _._2.contains) |
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
79 |
take (max_results + 1)).toList |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
80 |
for ((sym, _) <- results) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
81 |
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
|
82 |
if (results.length > max_results) results_panel.contents += new Label("...") |
50153 | 83 |
revalidate |
84 |
repaint |
|
50143
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
85 |
} |
50153 | 86 |
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
|
87 |
}, "Search Symbols") |
56609
5ac67041ccf8
capitalize more carefully, e.g. relevant for option "ML_exception_trace";
wenzelm
parents:
56600
diff
changeset
|
88 |
pages.map(p => |
5ac67041ccf8
capitalize more carefully, e.g. relevant for option "ML_exception_trace";
wenzelm
parents:
56600
diff
changeset
|
89 |
p.title = Word.implode(Word.explode('_', p.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
|
90 |
} |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
91 |
set_content(group_tabs) |
4ff5d795ed08
dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff
changeset
|
92 |
} |