# HG changeset patch
# User wenzelm
# Date 1661858313 -7200
# Node ID 752425c6957781a7c524f3918216b28e3a650eec
# Parent  04ce6cf2bd3b77d704eed036a515ca1ebd622a5a
clarified component structure, concerning initialization order;

diff -r 04ce6cf2bd3b -r 752425c69577 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Mon Aug 29 23:59:47 2022 +0200
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Aug 30 13:18:33 2022 +0200
@@ -19,36 +19,34 @@
   GUI_Thread.require {}
 
 
-  /* text area */
+  /* text area with zoom/resize */
 
   val pretty_text_area = new Pretty_Text_Area(view)
-  set_content(pretty_text_area)
 
   override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
+  private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
+  private def handle_resize(): Unit = GUI_Thread.require { pretty_text_area.zoom(zoom) }
+
+  private val delay_resize: Delay =
+    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
+
+  addComponentListener(new ComponentAdapter {
+    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
+  })
+
+  set_content(pretty_text_area)
+
 
   /* document build process */
 
   private val process_indicator = new Process_Indicator
 
 
-  /* resize */
-
-  private val delay_resize =
-    Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
-
-  addComponentListener(new ComponentAdapter {
-    override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
-    override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
-  })
-
-  private def handle_resize(): Unit =
-    GUI_Thread.require { pretty_text_area.zoom(zoom) }
-
-
   /* controls */
 
-  private val document_session =
+  private val document_session: GUI.Selector[String] =
     new GUI.Selector(JEdit_Sessions.sessions_structure().build_topological_order.sorted) {
       val title = "Session"
     }
@@ -63,8 +61,6 @@
       }
     }
 
-  private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
-
   private val controls =
     Wrap_Panel(List(document_session, process_indicator.component, build_button,
       pretty_text_area.search_label, pretty_text_area.search_field, zoom))
@@ -92,4 +88,3 @@
     delay_resize.revoke()
   }
 }
-