src/Tools/jEdit/src/symbols_dockable.scala
changeset 50151 5f5e74365f14
parent 50146 03f38212442a
child 50152 164af3238434
equal deleted inserted replaced
50147:8d2251b9a200 50151:5f5e74365f14
    37   }
    37   }
    38 
    38 
    39   val group_tabs = new TabbedPane {
    39   val group_tabs = new TabbedPane {
    40     pages ++= (for ((group, symbols) <- Symbol.groups) yield
    40     pages ++= (for ((group, symbols) <- Symbol.groups) yield
    41       {
    41       {
    42         new TabbedPane.Page(if (group == "") "Other" else group,
    42         new TabbedPane.Page(group,
    43           new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) },
    43           new FlowPanel { contents ++= symbols map (new Symbol_Component(_)) },
    44           ("" /: (symbols take 10 map Symbol.decode))(_ + _ + " "))
    44           (symbols take 10 map Symbol.decode).mkString(" "))
    45       }).toList.sortWith(_.title.toUpperCase <= _.title.toUpperCase)
    45       }).toList.sortWith(_.title <= _.title)
    46     pages += new TabbedPane.Page("Search", new BorderPanel {
    46     pages += new TabbedPane.Page("search", new BorderPanel {
    47       val search = new TextField(10)
    47       val search = new TextField(10)
    48       val results_panel = new FlowPanel
    48       val results_panel = new FlowPanel
    49       add(search, BorderPanel.Position.North)
    49       add(search, BorderPanel.Position.North)
    50       add(results_panel, BorderPanel.Position.Center)
    50       add(results_panel, BorderPanel.Position.Center)
    51       listenTo(search)
    51       listenTo(search)
    63           results_panel.revalidate
    63           results_panel.revalidate
    64           results_panel.repaint
    64           results_panel.repaint
    65         }
    65         }
    66       }
    66       }
    67     }, "Search Symbols")
    67     }, "Search Symbols")
       
    68     pages map (p => p.title = (space_explode('_', p.title) map Library.capitalize).mkString(" ") )
    68   }
    69   }
    69   set_content(group_tabs)
    70   set_content(group_tabs)
    70 }
    71 }