src/Tools/jEdit/src/symbols_dockable.scala
author immler
Wed, 21 Nov 2012 12:11:21 +0100
changeset 50151 5f5e74365f14
parent 50146 03f38212442a
child 50152 164af3238434
permissions -rw-r--r--
capitalize lowercase groups; tuned with mkString
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 =
50146
wenzelm
parents: 50145
diff changeset
    33
      new Font(Isabelle.font_family(),
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 }
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
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    39
  val group_tabs = 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
5f5e74365f14 capitalize lowercase groups;
immler
parents: 50146
diff changeset
    42
        new TabbedPane.Page(group,
50143
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    43
          new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) },
50151
5f5e74365f14 capitalize lowercase groups;
immler
parents: 50146
diff changeset
    44
          (symbols take 10 map Symbol.decode).mkString(" "))
5f5e74365f14 capitalize lowercase groups;
immler
parents: 50146
diff changeset
    45
      }).toList.sortWith(_.title <= _.title)
5f5e74365f14 capitalize lowercase groups;
immler
parents: 50146
diff changeset
    46
    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
    47
      val search = new TextField(10)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    48
      val results_panel = new FlowPanel
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    49
      add(search, BorderPanel.Position.North)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    50
      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
    51
      listenTo(search)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    52
      var last = search.text
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    53
      reactions += { case ValueChanged(`search`) =>
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    54
        if (search.text != last) {
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    55
          last = search.text
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    56
          results_panel.contents.clear
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    57
          val results =
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    58
            (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
    59
              take (max_results + 1)).toList
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    60
          for ((sym, _) <- results)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    61
            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
    62
          if (results.length > max_results) results_panel.contents += new Label("...")
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    63
          results_panel.revalidate
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    64
          results_panel.repaint
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
      }
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    67
    }, "Search Symbols")
50151
5f5e74365f14 capitalize lowercase groups;
immler
parents: 50146
diff changeset
    68
    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
    69
  }
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    70
  set_content(group_tabs)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols;
immler
parents:
diff changeset
    71
}