# HG changeset patch # User wenzelm # Date 1646320707 -3600 # Node ID c05f0e8a54de9e9fd000fcefc708def9d38d578e # Parent 1ced8ee860e2619e8f381e19abdd069df3bdd97b misc tuning, based on suggestions by IntelliJ IDEA; diff -r 1ced8ee860e2 -r c05f0e8a54de src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Thu Mar 03 16:05:02 2022 +0100 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Thu Mar 03 16:18:27 2022 +0100 @@ -27,12 +27,12 @@ private val abbrevs_panel = new Abbrevs_Panel private val abbrevs_refresh_delay = - Delay.last(PIDE.options.seconds("editor_update_delay"), gui = true) { abbrevs_panel.refresh } + Delay.last(PIDE.options.seconds("editor_update_delay"), gui = true) { abbrevs_panel.refresh() } private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button { - def update_font: Unit = { font = GUI.font(size = font_size) } - update_font + def update_font(): Unit = { font = GUI.font(size = font_size) } + update_font() text = "" + HTML.output(Symbol.decode(txt)) + "" action = @@ -51,7 +51,7 @@ { private var abbrevs: Thy_Header.Abbrevs = Nil - def refresh: Unit = GUI_Thread.require { + def refresh(): Unit = GUI_Thread.require { val abbrevs1 = Isabelle.buffer_syntax(view.getBuffer).getOrElse(Outer_Syntax.empty).abbrevs if (abbrevs != abbrevs1) { @@ -75,7 +75,7 @@ } } - refresh + refresh() } @@ -83,7 +83,7 @@ private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button { - def update_font: Unit = + def update_font(): Unit = { font = Symbol.symbols.fonts.get(symbol) match { @@ -91,7 +91,7 @@ case Some(font_family) => GUI.font(family = font_family, size = font_size) } } - update_font + update_font() action = Action(Symbol.decode(symbol)) { @@ -122,14 +122,14 @@ private class Search_Panel extends BorderPanel { val search_field = new TextField(10) - val results_panel = Wrap_Panel(Nil, Wrap_Panel.Alignment.Center) + val results_panel: Wrap_Panel = Wrap_Panel(Nil, Wrap_Panel.Alignment.Center) layout(search_field) = BorderPanel.Position.North layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center - val search_space = + private val search_space = for (entry <- Symbol.symbols.entries if entry.code.isDefined) yield entry.symbol -> Word.lowercase(entry.symbol) - val search_delay = + val search_delay: Delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { val search_words = Word.explode(Word.lowercase(search_field.text)) val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0 @@ -184,7 +184,7 @@ /* main */ private val edit_bus_handler: EBComponent = - new EBComponent { def handleMessage(msg: EBMessage): Unit = abbrevs_refresh_delay.invoke() } + (_: EBMessage) => abbrevs_refresh_delay.invoke() private val main = Session.Consumer[Any](getClass.getName) { @@ -195,8 +195,8 @@ { case c0: javax.swing.JComponent => Component.wrap(c0) match { - case c: Abbrev_Component => c.update_font - case c: Symbol_Component => c.update_font + case c: Abbrev_Component => c.update_font() + case c: Symbol_Component => c.update_font() case _ => } case _ =>