src/Tools/jEdit/src/symbols_dockable.scala
author wenzelm
Sat, 24 Nov 2012 16:13:21 +0100
changeset 50185 820673500454
parent 50155 e2c08f20d00e
child 50186 f83cab68c788
permissions -rw-r--r--
avoid showing semantic aspects of Unicode -- Isabelle/Scala merely (ab)uses the low-level rendering model (codepoint + font);
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
{
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
  {
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    28
    val dec = Symbol.decode(symbol)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    29
    font =
50152
164af3238434 respect font property for symbols
immler
parents: 50151
diff changeset
    30
      new Font(Symbol.fonts.getOrElse(symbol, Isabelle.font_family()),
50146
wenzelm
parents: 50145
diff changeset
    31
        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
    32
    action = Action(dec) { view.getTextArea.setSelectedText(dec); view.getTextArea.requestFocus }
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
    33
    tooltip =
820673500454 avoid showing semantic aspects of Unicode -- Isabelle/Scala merely (ab)uses the low-level rendering model (codepoint + font);
wenzelm
parents: 50155
diff changeset
    34
      symbol +
820673500454 avoid showing semantic aspects of Unicode -- Isabelle/Scala merely (ab)uses the low-level rendering model (codepoint + font);
wenzelm
parents: 50155
diff changeset
    35
        (if (Symbol.abbrevs.isDefinedAt(symbol)) " abbrev: " + Symbol.abbrevs(symbol) else "")
50143
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    36
  }
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    37
50153
e6121a825db8 delayed search to improve reactivity
immler
parents: 50152
diff changeset
    38
  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
    39
    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
    40
      {
50151
5f5e74365f14 capitalize lowercase groups;
immler
parents: 50146
diff changeset
    41
        new TabbedPane.Page(group,
50154
ab5272955b3b removed (unicode) tooltips: can not adjust font in basic swing tooltip
immler
parents: 50153
diff changeset
    42
          new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) })
50151
5f5e74365f14 capitalize lowercase groups;
immler
parents: 50146
diff changeset
    43
      }).toList.sortWith(_.title <= _.title)
5f5e74365f14 capitalize lowercase groups;
immler
parents: 50146
diff changeset
    44
    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
    45
      val search = new TextField(10)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    46
      val results_panel = new FlowPanel
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    47
      add(search, BorderPanel.Position.North)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    48
      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
    49
      listenTo(search)
50153
e6121a825db8 delayed search to improve reactivity
immler
parents: 50152
diff changeset
    50
      val delay_search =
e6121a825db8 delayed search to improve reactivity
immler
parents: 50152
diff changeset
    51
        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
    52
          results_panel.contents.clear
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    53
          val results =
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    54
            (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
    55
              take (max_results + 1)).toList
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    56
          for ((sym, _) <- results)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    57
            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
    58
          if (results.length > max_results) results_panel.contents += new Label("...")
50153
e6121a825db8 delayed search to improve reactivity
immler
parents: 50152
diff changeset
    59
          revalidate
e6121a825db8 delayed search to improve reactivity
immler
parents: 50152
diff changeset
    60
          repaint
50143
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    61
        }
50153
e6121a825db8 delayed search to improve reactivity
immler
parents: 50152
diff changeset
    62
      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
    63
    }, "Search Symbols")
50151
5f5e74365f14 capitalize lowercase groups;
immler
parents: 50146
diff changeset
    64
    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
    65
  }
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    66
  set_content(group_tabs)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    67
}