src/Tools/jEdit/src/output_dockable.scala
changeset 75393 87ebf5a50283
parent 73987 fc363a3b690a
child 75809 1dd5d4f4b69e
--- a/src/Tools/jEdit/src/output_dockable.scala	Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Apr 01 17:06:10 2022 +0200
@@ -18,8 +18,7 @@
 import org.gjt.sp.jedit.View
 
 
-class Output_Dockable(view: View, position: String) extends Dockable(view, position)
-{
+class Output_Dockable(view: View, position: String) extends Dockable(view, position) {
   /* component state -- owned by GUI thread */
 
   private var do_update = true
@@ -34,16 +33,14 @@
   override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
 
-  private def handle_resize(): Unit =
-  {
+  private def handle_resize(): Unit = {
     GUI_Thread.require {}
 
     pretty_text_area.resize(
       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
   }
 
-  private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit =
-  {
+  private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = {
     GUI_Thread.require {}
 
     for {
@@ -72,8 +69,7 @@
   /* controls */
 
   private def output_state: Boolean = PIDE.options.bool("editor_output_state")
-  private def output_state_=(b: Boolean): Unit =
-  {
+  private def output_state_=(b: Boolean): Unit = {
     if (output_state != b) {
       PIDE.options.bool("editor_output_state") = b
       PIDE.session.update_options(PIDE.options.value)
@@ -82,8 +78,7 @@
     }
   }
 
-  private val output_state_button = new CheckBox("Proof state")
-  {
+  private val output_state_button = new CheckBox("Proof state") {
     tooltip = "Output of proof state (normally shown on State panel)"
     reactions += { case ButtonClicked(_) => output_state = selected }
     selected = output_state
@@ -130,16 +125,14 @@
         GUI_Thread.later { handle_update(do_update, None) }
     }
 
-  override def init(): Unit =
-  {
+  override def init(): Unit = {
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
     PIDE.session.caret_focus += main
     handle_update(true, None)
   }
 
-  override def exit(): Unit =
-  {
+  override def exit(): Unit = {
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
     PIDE.session.caret_focus -= main