src/Tools/jEdit/src/symbols_dockable.scala
author wenzelm
Sat, 24 Nov 2012 18:29:19 +0100
changeset 50192 22d0f64362a5
parent 50191 8b5a256859af
child 50205 788c8263e634
permissions -rw-r--r--
tuned -- Symbol.groups already sorted;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
{
50145
88ba14e563d4 accomodate scala-2.10.0-RC2 with its slight reform on for-syntax;
wenzelm
parents: 50143
diff changeset
    20
  val searchspace =
88ba14e563d4 accomodate scala-2.10.0-RC2 with its slight reform on for-syntax;
wenzelm
parents: 50143
diff changeset
    21
    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
    22
      yield (sym, sym.toLowerCase)
50143
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    23
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    24
  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
    25
  {
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    26
    private val decoded = Symbol.decode(symbol)
50191
8b5a256859af more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
wenzelm
parents: 50190
diff changeset
    27
    private val font_size = Isabelle.font_size("jedit_font_scale").round
8b5a256859af more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
wenzelm
parents: 50190
diff changeset
    28
50143
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    29
    font =
50191
8b5a256859af more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
wenzelm
parents: 50190
diff changeset
    30
      Symbol.fonts.get(symbol) match {
8b5a256859af more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
wenzelm
parents: 50190
diff changeset
    31
        case None => Isabelle_System.get_font(size = font_size)
8b5a256859af more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
wenzelm
parents: 50190
diff changeset
    32
        case Some(font_family) => Isabelle_System.get_font(family = font_family, size = font_size)
8b5a256859af more robust default font -- user might have switched jEdit TextArea to another font that lacks glyphs;
wenzelm
parents: 50190
diff changeset
    33
      }
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    34
    action =
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    35
      Action(decoded) {
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    36
        val text_area = view.getTextArea
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    37
        if (Token_Markup.is_control_style(decoded))
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    38
          Token_Markup.edit_control_style(text_area, decoded)
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    39
        else text_area.setSelectedText(decoded)
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    40
        text_area.requestFocus
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    41
      }
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
    42
    tooltip =
50186
f83cab68c788 recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents: 50185
diff changeset
    43
      JEdit_Lib.wrap_tooltip(
f83cab68c788 recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents: 50185
diff changeset
    44
        symbol +
f83cab68c788 recovered some tooltip wrapping from e2762f962042, with multi-line support via HTML.encode;
wenzelm
parents: 50185
diff changeset
    45
          (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
    46
  }
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    47
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    48
  private class Reset_Component extends Button
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    49
  {
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    50
    action = Action("Reset") {
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    51
      val text_area = view.getTextArea
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    52
      Token_Markup.edit_control_style(text_area, "")
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    53
      text_area.requestFocus
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
    tooltip = "Reset control symbols within text"
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
50153
e6121a825db8 delayed search to improve reactivity
immler
parents: 50152
diff changeset
    58
  val group_tabs: TabbedPane = new TabbedPane {
50192
22d0f64362a5 tuned -- Symbol.groups already sorted;
wenzelm
parents: 50191
diff changeset
    59
    pages ++=
22d0f64362a5 tuned -- Symbol.groups already sorted;
wenzelm
parents: 50191
diff changeset
    60
      Symbol.groups map { case (group, symbols) =>
50151
5f5e74365f14 capitalize lowercase groups;
immler
parents: 50146
diff changeset
    61
        new TabbedPane.Page(group,
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    62
          new FlowPanel {
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    63
            contents ++= symbols.map(new Symbol_Component(_))
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50186
diff changeset
    64
            if (group == "control") contents += new Reset_Component
50189
5ab700fd5128 avoid empty tooltip;
wenzelm
parents: 50187
diff changeset
    65
          }, null)
50192
22d0f64362a5 tuned -- Symbol.groups already sorted;
wenzelm
parents: 50191
diff changeset
    66
      }
50151
5f5e74365f14 capitalize lowercase groups;
immler
parents: 50146
diff changeset
    67
    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
    68
      val search = new TextField(10)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    69
      val results_panel = new FlowPanel
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    70
      add(search, BorderPanel.Position.North)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    71
      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
    72
      listenTo(search)
50153
e6121a825db8 delayed search to improve reactivity
immler
parents: 50152
diff changeset
    73
      val delay_search =
e6121a825db8 delayed search to improve reactivity
immler
parents: 50152
diff changeset
    74
        Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
50190
0d7f0d8fd63b added option jedit_symbols_search_limit;
wenzelm
parents: 50189
diff changeset
    75
          val max_results = Isabelle.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
    76
          results_panel.contents.clear
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    77
          val results =
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    78
            (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
    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
e6121a825db8 delayed search to improve reactivity
immler
parents: 50152
diff changeset
    83
          revalidate
e6121a825db8 delayed search to improve reactivity
immler
parents: 50152
diff changeset
    84
          repaint
50143
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    85
        }
50153
e6121a825db8 delayed search to improve reactivity
immler
parents: 50152
diff changeset
    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")
50151
5f5e74365f14 capitalize lowercase groups;
immler
parents: 50146
diff changeset
    88
    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
    89
  }
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    90
  set_content(group_tabs)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    91
}