--- 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()
}
}
-