--- a/src/Tools/jEdit/src/debugger_dockable.scala Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Thu Nov 07 13:22:59 2024 +0100
@@ -68,8 +68,6 @@
private val output: Output_Area =
new Output_Area(view, root_name = "Threads", split = true) {
- override def handle_resize(): Unit = pretty_text_area.zoom(zoom)
-
override def handle_update(): Unit = {
val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
val (new_threads, new_output) = debugger.status(tree_selection())
@@ -231,17 +229,13 @@
tooltip = "Official Standard ML instead of Isabelle/ML"
}
- private val zoom =
- new Font_Info.Zoom { override def changed(): Unit = output.handle_resize() }
-
private val controls =
Wrap_Panel(
List(
break_button, continue_button, step_button, step_over_button, step_out_button,
context_label, Component.wrap(context_field),
expression_label, Component.wrap(expression_field), eval_button, sml_button) :::
- output.pretty_text_area.search_components :::
- List(output.pretty_text_area.search_field, zoom))
+ output.pretty_text_area.search_zoom_components)
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/document_dockable.scala Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Thu Nov 07 13:22:59 2024 +0100
@@ -91,8 +91,7 @@
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 def handle_resize(): Unit = pretty_text_area.zoom()
private val delay_resize: Delay =
Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
@@ -352,7 +351,7 @@
override def clicked(): Unit = cancel_process()
}
- private val output_controls = Wrap_Panel(List(cancel_button, zoom))
+ private val output_controls = Wrap_Panel(List(cancel_button, pretty_text_area.zoom_component))
private val output_page =
new TabbedPane.Page("Output", new BorderPanel {
--- a/src/Tools/jEdit/src/info_dockable.scala Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Thu Nov 07 13:22:59 2024 +0100
@@ -72,10 +72,7 @@
pretty_text_area.update(snapshot, results, info)
- 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 def handle_resize(): Unit = pretty_text_area.zoom()
/* resize */
@@ -88,7 +85,7 @@
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
- private val controls = Wrap_Panel(pretty_text_area.search_components ::: List(zoom))
+ private val controls = Wrap_Panel(pretty_text_area.search_zoom_components)
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/output_area.scala Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala Thu Nov 07 13:22:59 2024 +0100
@@ -37,7 +37,7 @@
val pretty_text_area: Pretty_Text_Area = new Pretty_Text_Area(view)
- def handle_resize(): Unit = ()
+ def handle_resize(): Unit = pretty_text_area.zoom()
def handle_update(): Unit = ()
lazy val delay_resize: Delay =
--- a/src/Tools/jEdit/src/output_dockable.scala Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu Nov 07 13:22:59 2024 +0100
@@ -30,8 +30,7 @@
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
- private def handle_resize(): Unit =
- GUI_Thread.require { pretty_text_area.zoom(zoom) }
+ private def handle_resize(): Unit = pretty_text_area.zoom()
private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = {
GUI_Thread.require {}
@@ -78,12 +77,10 @@
override def clicked(): Unit = handle_update(true, None)
}
- private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
-
private val controls =
Wrap_Panel(
List(output_state_button, auto_hovering_button, auto_update_button, update_button) :::
- pretty_text_area.search_components ::: List(zoom))
+ pretty_text_area.search_zoom_components)
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 07 13:22:59 2024 +0100
@@ -120,9 +120,6 @@
refresh()
}
- def zoom(zoom: GUI.Zoom): Unit =
- resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale"), zoom = zoom))
-
def update(
base_snapshot: Document.Snapshot,
base_results: Command.Results,
@@ -146,7 +143,7 @@
if (current_body.isEmpty) None else Some(() => detach())
- /* common GUI components */
+ /* search */
val search_label: Component = new Label("Search:") {
tooltip = "Search and highlight output via regular expression"
@@ -166,8 +163,6 @@
setFont(GUI.imitate_font(getFont, scale = 1.2))
})
- def search_components: List[Component] = List(search_label, search_field)
-
private val search_field_foreground = search_field.foreground
private def search_action(text_field: JTextField): Unit = {
@@ -188,6 +183,22 @@
}
+ /* zoom */
+
+ val zoom_component: GUI.Zoom =
+ new Font_Info.Zoom { override def changed(): Unit = zoom() }
+
+ def zoom(zoom: GUI.Zoom = zoom_component): Unit =
+ resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale"), zoom = zoom))
+
+
+ /* common GUI components */
+
+ def search_components: List[Component] = List(search_label, search_field)
+
+ def search_zoom_components: List[Component] = List(search_label, search_field, zoom_component)
+
+
/* key handling */
override def getInputMethodRequests: InputMethodRequests = null
--- a/src/Tools/jEdit/src/query_dockable.scala Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Thu Nov 07 13:22:59 2024 +0100
@@ -300,7 +300,7 @@
private def handle_resize(): Unit =
GUI_Thread.require {
- if (operations != null) operations.foreach(_.pretty_text_area.zoom(zoom))
+ if (operations != null) operations.foreach(_.pretty_text_area.zoom(zoom = zoom))
}
private val delay_resize =
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Thu Nov 07 13:22:59 2024 +0100
@@ -61,11 +61,7 @@
new Simplifier_Trace_Window(view, current_snapshot, trace)
}
- private def handle_resize(): Unit = {
- GUI_Thread.later {
- text_area.resize(Font_Info.main(scale = PIDE.options.real("jedit_font_scale")))
- }
- }
+ private def handle_resize(): Unit = text_area.zoom()
private def handle_update(follow: Boolean): Unit = {
val (new_snapshot, new_command, new_results, new_id) =
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Thu Nov 07 13:22:59 2024 +0100
@@ -130,7 +130,6 @@
GUI_Thread.require {}
private val pretty_text_area = new Pretty_Text_Area(view)
- private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
size = new Dimension(500, 500)
contents = new BorderPanel {
@@ -155,8 +154,7 @@
pretty_text_area.update(snapshot, Command.Results.empty, xml)
}
- def handle_resize(): Unit =
- GUI_Thread.later { pretty_text_area.zoom(zoom) }
+ def handle_resize(): Unit = pretty_text_area.zoom()
/* resize */
@@ -172,7 +170,7 @@
/* controls */
- private val controls = Wrap_Panel(pretty_text_area.search_components ::: List(zoom))
+ private val controls = Wrap_Panel(pretty_text_area.search_zoom_components)
peer.add(controls.peer, BorderLayout.NORTH)
}
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Nov 07 13:22:59 2024 +0100
@@ -61,8 +61,7 @@
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
- private def handle_resize(): Unit =
- GUI_Thread.require { pretty_text_area.zoom(zoom) }
+ private def handle_resize(): Unit = pretty_text_area.zoom()
/* controls */
@@ -122,12 +121,11 @@
override def clicked(): Unit = sledgehammer.locate_query()
}
- private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
-
private val controls =
Wrap_Panel(
List(provers_label, Component.wrap(provers), isar_proofs, try0,
- process_indicator.component, apply_query, cancel_query, locate_query, zoom))
+ process_indicator.component, apply_query, cancel_query, locate_query,
+ pretty_text_area.zoom_component))
add(controls.peer, BorderLayout.NORTH)
--- a/src/Tools/jEdit/src/state_dockable.scala Thu Nov 07 12:35:55 2024 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Thu Nov 07 13:22:59 2024 +0100
@@ -42,8 +42,7 @@
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
- private def handle_resize(): Unit =
- GUI_Thread.require { pretty_text_area.zoom(zoom) }
+ private def handle_resize(): Unit = pretty_text_area.zoom()
/* update */
@@ -93,12 +92,10 @@
override def clicked(): Unit = print_state.locate_query()
}
- private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
-
private val controls =
Wrap_Panel(
List(auto_update_button, update_button, locate_button) :::
- pretty_text_area.search_components ::: List(zoom))
+ pretty_text_area.search_zoom_components)
add(controls.peer, BorderLayout.NORTH)