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