src/Tools/jEdit/src/symbols_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 63926 70973a1b4ec0
child 65259 41d12227d5dc
permissions -rw-r--r--
tuned signature;
immler@50143
     1
/*  Title:      Tools/jEdit/src/symbols_dockable.scala
immler@50143
     2
    Author:     Fabian Immler
immler@50143
     3
immler@50143
     4
Dockable window for Symbol Palette.
immler@50143
     5
*/
immler@50143
     6
immler@50143
     7
package isabelle.jedit
immler@50143
     8
immler@50143
     9
immler@50143
    10
import isabelle._
immler@50143
    11
wenzelm@56755
    12
import scala.swing.event.{SelectionChanged, ValueChanged}
wenzelm@63874
    13
import scala.swing.{Component, Action, Button, TabbedPane, TextField, BorderPanel,
wenzelm@63874
    14
  Label, ScrollPane}
immler@50143
    15
wenzelm@63872
    16
import org.gjt.sp.jedit.{EditBus, EBComponent, EBMessage, View}
wenzelm@50299
    17
wenzelm@50299
    18
immler@50143
    19
class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
immler@50143
    20
{
wenzelm@63870
    21
  private def font_size: Int =
wenzelm@63870
    22
    Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
wenzelm@63870
    23
wenzelm@63872
    24
wenzelm@63877
    25
  /* abbrevs */
wenzelm@63872
    26
wenzelm@63872
    27
  private val abbrevs_panel = new Abbrevs_Panel
wenzelm@63872
    28
wenzelm@63872
    29
  private val abbrevs_refresh_delay =
wenzelm@63872
    30
    GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh }
wenzelm@63872
    31
wenzelm@63873
    32
  private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button
wenzelm@63870
    33
  {
wenzelm@63874
    34
    def update_font { font = GUI.font(size = font_size) }
wenzelm@63874
    35
    update_font
wenzelm@63874
    36
wenzelm@63873
    37
    text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>"
wenzelm@63870
    38
    action =
wenzelm@63870
    39
      Action(text) {
wenzelm@63870
    40
        val text_area = view.getTextArea
wenzelm@63873
    41
        val (s1, s2) =
wenzelm@63873
    42
          Completion.split_template(Isabelle_Encoding.maybe_decode(text_area.getBuffer, txt))
wenzelm@63873
    43
        text_area.setSelectedText(s1 + s2)
wenzelm@63870
    44
        text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
wenzelm@63870
    45
        text_area.requestFocus
wenzelm@63870
    46
      }
wenzelm@63873
    47
    tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a)))
wenzelm@63870
    48
  }
wenzelm@63870
    49
wenzelm@63870
    50
  private class Abbrevs_Panel extends Wrap_Panel
wenzelm@63870
    51
  {
wenzelm@63870
    52
    private var abbrevs: Thy_Header.Abbrevs = Nil
wenzelm@63870
    53
wenzelm@63872
    54
    def refresh: Unit = GUI_Thread.require {
wenzelm@63873
    55
      val abbrevs1 = Isabelle.buffer_syntax(view.getBuffer).getOrElse(Outer_Syntax.empty).abbrevs
wenzelm@63873
    56
wenzelm@63870
    57
      if (abbrevs != abbrevs1) {
wenzelm@63870
    58
        abbrevs = abbrevs1
wenzelm@63870
    59
wenzelm@63873
    60
        val entries: List[(String, List[String])] =
wenzelm@63873
    61
          Multi_Map(
wenzelm@63873
    62
            (for {
wenzelm@63873
    63
              (abbr, txt0) <- abbrevs
wenzelm@63926
    64
              txt = Symbol.encode(txt0)
wenzelm@63873
    65
              if !Symbol.iterator(txt).
wenzelm@63873
    66
                forall(s => s.length == 1 && s(0) != Completion.caret_indicator)
wenzelm@63873
    67
            } yield (txt, abbr)): _*).iterator_list.toList
wenzelm@63873
    68
wenzelm@63870
    69
        contents.clear
wenzelm@63873
    70
        for ((txt, abbrs) <- entries.sortBy(_._1))
wenzelm@63873
    71
          contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted)
wenzelm@63870
    72
wenzelm@63870
    73
        revalidate
wenzelm@63870
    74
        repaint
wenzelm@63870
    75
      }
wenzelm@63870
    76
    }
wenzelm@63872
    77
wenzelm@63870
    78
    refresh
wenzelm@63870
    79
  }
wenzelm@63870
    80
wenzelm@63872
    81
wenzelm@63872
    82
  /* symbols */
wenzelm@63872
    83
wenzelm@62104
    84
  private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button
immler@50143
    85
  {
wenzelm@63874
    86
    def update_font
wenzelm@63874
    87
    {
wenzelm@63874
    88
      font =
wenzelm@63874
    89
        Symbol.fonts.get(symbol) match {
wenzelm@63874
    90
          case None => GUI.font(size = font_size)
wenzelm@63874
    91
          case Some(font_family) => GUI.font(family = font_family, size = font_size)
wenzelm@63874
    92
        }
wenzelm@63874
    93
    }
wenzelm@63874
    94
    update_font
wenzelm@63874
    95
wenzelm@50187
    96
    action =
wenzelm@62104
    97
      Action(Symbol.decode(symbol)) {
wenzelm@50187
    98
        val text_area = view.getTextArea
wenzelm@62104
    99
        if (is_control && HTML.control.isDefinedAt(symbol))
wenzelm@62104
   100
          Token_Markup.edit_control_style(text_area, symbol)
wenzelm@62104
   101
        else
wenzelm@62104
   102
          text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
wenzelm@50187
   103
        text_area.requestFocus
wenzelm@50187
   104
      }
wenzelm@56622
   105
    tooltip =
wenzelm@56622
   106
      GUI.tooltip_lines(
wenzelm@56622
   107
        cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a)))
immler@50143
   108
  }
immler@50143
   109
wenzelm@50187
   110
  private class Reset_Component extends Button
wenzelm@50187
   111
  {
wenzelm@50187
   112
    action = Action("Reset") {
wenzelm@50187
   113
      val text_area = view.getTextArea
wenzelm@50187
   114
      Token_Markup.edit_control_style(text_area, "")
wenzelm@50187
   115
      text_area.requestFocus
wenzelm@50187
   116
    }
wenzelm@50187
   117
    tooltip = "Reset control symbols within text"
wenzelm@50187
   118
  }
wenzelm@50187
   119
wenzelm@63872
   120
wenzelm@63877
   121
  /* search */
wenzelm@63877
   122
wenzelm@63877
   123
  private class Search_Panel extends BorderPanel {
wenzelm@63877
   124
    val search_field = new TextField(10)
wenzelm@63877
   125
    val results_panel = new Wrap_Panel
wenzelm@63877
   126
    layout(search_field) = BorderPanel.Position.North
wenzelm@63877
   127
    layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
wenzelm@63877
   128
wenzelm@63877
   129
    val search_space =
wenzelm@63877
   130
      (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
wenzelm@63877
   131
    val search_delay =
wenzelm@63877
   132
      GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
wenzelm@63877
   133
        val search_words = Word.explode(Word.lowercase(search_field.text))
wenzelm@63877
   134
        val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
wenzelm@63877
   135
        val results =
wenzelm@63877
   136
          for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym
wenzelm@63877
   137
wenzelm@63877
   138
        results_panel.contents.clear
wenzelm@63877
   139
        for (sym <- results.take(search_limit))
wenzelm@63877
   140
          results_panel.contents += new Symbol_Component(sym, false)
wenzelm@63877
   141
        if (results.length > search_limit)
wenzelm@63877
   142
          results_panel.contents +=
wenzelm@63877
   143
            new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
wenzelm@63877
   144
        revalidate
wenzelm@63877
   145
        repaint
wenzelm@63877
   146
      }
wenzelm@63877
   147
      search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
wenzelm@63877
   148
  }
wenzelm@63877
   149
wenzelm@63877
   150
wenzelm@63872
   151
  /* tabs */
wenzelm@63870
   152
wenzelm@56756
   153
  private val group_tabs: TabbedPane = new TabbedPane {
wenzelm@63870
   154
    pages += new TabbedPane.Page("abbrevs", abbrevs_panel)
wenzelm@63870
   155
wenzelm@50192
   156
    pages ++=
wenzelm@56753
   157
      Symbol.groups.map({ case (group, symbols) =>
immler@50151
   158
        new TabbedPane.Page(group,
wenzelm@53713
   159
          new ScrollPane(new Wrap_Panel {
wenzelm@62024
   160
            val control = group == "control"
wenzelm@62024
   161
            contents ++= symbols.map(new Symbol_Component(_, control))
wenzelm@62024
   162
            if (control) contents += new Reset_Component
wenzelm@53713
   163
          }), null)
wenzelm@56753
   164
      })
wenzelm@56753
   165
wenzelm@63877
   166
    val search_panel = new Search_Panel
wenzelm@63877
   167
    val search_page = new TabbedPane.Page("search", search_panel, "Search Symbols")
wenzelm@56755
   168
    pages += search_page
wenzelm@56755
   169
wenzelm@56755
   170
    listenTo(selection)
wenzelm@56755
   171
    reactions += {
wenzelm@63877
   172
      case SelectionChanged(_) if selection.page == search_page =>
wenzelm@63877
   173
        search_panel.search_field.requestFocus
wenzelm@56755
   174
    }
wenzelm@56755
   175
wenzelm@56756
   176
    for (page <- pages)
wenzelm@56756
   177
      page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_)))
immler@50143
   178
  }
immler@50143
   179
  set_content(group_tabs)
wenzelm@63872
   180
wenzelm@63872
   181
wenzelm@63872
   182
wenzelm@63872
   183
  /* main */
wenzelm@63872
   184
wenzelm@63872
   185
  private val edit_bus_handler: EBComponent =
wenzelm@63872
   186
    new EBComponent { def handleMessage(msg: EBMessage) { abbrevs_refresh_delay.invoke() } }
wenzelm@63872
   187
wenzelm@63872
   188
  private val main =
wenzelm@63872
   189
    Session.Consumer[Any](getClass.getName) {
wenzelm@63874
   190
      case _: Session.Global_Options =>
wenzelm@63874
   191
        GUI_Thread.later {
wenzelm@63874
   192
          val comp = group_tabs.peer
wenzelm@63874
   193
          GUI.traverse_components(comp,
wenzelm@63874
   194
            {
wenzelm@63874
   195
              case c0: javax.swing.JComponent =>
wenzelm@63874
   196
                Component.wrap(c0) match {
wenzelm@63874
   197
                  case c: Abbrev_Component => c.update_font
wenzelm@63874
   198
                  case c: Symbol_Component => c.update_font
wenzelm@63874
   199
                  case _ =>
wenzelm@63874
   200
                }
wenzelm@63874
   201
              case _ =>
wenzelm@63874
   202
            })
wenzelm@63874
   203
          comp.revalidate
wenzelm@63874
   204
          comp.repaint()
wenzelm@63874
   205
        }
wenzelm@63872
   206
      case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke()
wenzelm@63872
   207
    }
wenzelm@63872
   208
wenzelm@63872
   209
  override def init()
wenzelm@63872
   210
  {
wenzelm@63872
   211
    EditBus.addToBus(edit_bus_handler)
wenzelm@63874
   212
    PIDE.session.global_options += main
wenzelm@63872
   213
    PIDE.session.commands_changed += main
wenzelm@63872
   214
  }
wenzelm@63872
   215
wenzelm@63872
   216
  override def exit()
wenzelm@63872
   217
  {
wenzelm@63872
   218
    EditBus.removeFromBus(edit_bus_handler)
wenzelm@63874
   219
    PIDE.session.global_options -= main
wenzelm@63872
   220
    PIDE.session.commands_changed -= main
wenzelm@63872
   221
  }
immler@50143
   222
}