src/Tools/jEdit/src/symbols_dockable.scala
changeset 56609 5ac67041ccf8
parent 56600 628e039cc34d
child 56622 891d1b8b64fb
equal deleted inserted replaced
56608:8e3c848008fa 56609:5ac67041ccf8
    83           revalidate
    83           revalidate
    84           repaint
    84           repaint
    85         }
    85         }
    86       reactions += { case ValueChanged(`search`) => delay_search.invoke() }
    86       reactions += { case ValueChanged(`search`) => delay_search.invoke() }
    87     }, "Search Symbols")
    87     }, "Search Symbols")
    88     pages.map(p => p.title = Word.implode(Word.explode('_', p.title).map(Word.capitalize(_))))
    88     pages.map(p =>
       
    89       p.title = Word.implode(Word.explode('_', p.title).map(Word.perhaps_capitalize(_))))
    89   }
    90   }
    90   set_content(group_tabs)
    91   set_content(group_tabs)
    91 }
    92 }