--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Mar 01 22:22:12 2021 +0100
@@ -37,7 +37,7 @@
private val process_indicator = new Process_Indicator
- private def consume_status(status: Query_Operation.Status.Value)
+ private def consume_status(status: Query_Operation.Status.Value): Unit =
{
status match {
case Query_Operation.Status.WAITING =>
@@ -61,11 +61,11 @@
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
- override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
- private def handle_resize()
+ private def handle_resize(): Unit =
{
GUI_Thread.require {}
@@ -76,7 +76,8 @@
/* controls */
- private def clicked {
+ private def clicked: Unit =
+ {
provers.addCurrentToHistory()
PIDE.options.string("sledgehammer_provers") = provers.getText
sledgehammer.apply_query(
@@ -91,7 +92,7 @@
}
private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
- override def processKeyEvent(evt: KeyEvent)
+ override def processKeyEvent(evt: KeyEvent): Unit =
{
if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
super.processKeyEvent(evt)
@@ -100,7 +101,7 @@
setColumns(30)
}
- private def update_provers()
+ private def update_provers(): Unit =
{
val new_provers = PIDE.options.string("sledgehammer_provers")
if (new_provers != provers.getText) {
@@ -144,7 +145,7 @@
add(controls.peer, BorderLayout.NORTH)
- override def focusOnDefaultComponent() { provers.requestFocus }
+ override def focusOnDefaultComponent(): Unit = provers.requestFocus
/* main */
@@ -154,7 +155,7 @@
case _: Session.Global_Options => GUI_Thread.later { update_provers(); handle_resize() }
}
- override def init()
+ override def init(): Unit =
{
PIDE.session.global_options += main
update_provers()
@@ -162,7 +163,7 @@
sledgehammer.activate()
}
- override def exit()
+ override def exit(): Unit =
{
sledgehammer.deactivate()
PIDE.session.global_options -= main