# HG changeset patch # User wenzelm # Date 1660386758 -7200 # Node ID 29441f2bfe810f455e329506ac9187ee506c2d9b # Parent 7f6803788de3aa01c4e6dfcd205a7b028aa3eff0 clarified signature: more explicit types; more robust zoom.factor: work with uninitialized GUI components; diff -r 7f6803788de3 -r 29441f2bfe81 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Pure/GUI/gui.scala Sat Aug 13 12:32:38 2022 +0200 @@ -111,14 +111,20 @@ } - /* zoom box */ + /* variations on ComboBox */ + + class Selector[A](val entries: List[A]) extends ComboBox[A](entries) { + def changed(): Unit = {} + + listenTo(selection) + reactions += { case SelectionChanged(_) => changed() } + } private val Zoom_Factor = "([0-9]+)%?".r - abstract class Zoom_Box extends ComboBox[String]( + class Zoom extends Selector[String]( List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%") ) { - def changed(): Unit def factor: Int = parse(selection.item) private def parse(text: String): Int = @@ -145,9 +151,6 @@ } selection.index = 3 - - listenTo(selection) - reactions += { case SelectionChanged(_) => changed() } } diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/Graphview/graph_panel.scala --- a/src/Tools/Graphview/graph_panel.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/Graphview/graph_panel.scala Sat Aug 13 12:32:38 2022 +0200 @@ -298,7 +298,7 @@ tooltip = "Save current graph layout as PNG or PDF" } - private val zoom = new GUI.Zoom_Box { def changed(): Unit = rescale(0.01 * factor) } + private val zoom = new GUI.Zoom { override def changed(): Unit = rescale(0.01 * factor) } private val fit_window = new Button { action = Action("Fit to window") { fit_to_window() } diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Sat Aug 13 12:32:38 2022 +0200 @@ -73,7 +73,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.factor) } + GUI_Thread.require { pretty_text_area.zoom(zoom) } private def handle_update(): Unit = { GUI_Thread.require {} @@ -262,7 +262,7 @@ selected = false } - private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() } + private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } private val controls = Wrap_Panel( diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/document_dockable.scala Sat Aug 13 12:32:38 2022 +0200 @@ -12,8 +12,8 @@ import java.awt.BorderLayout import java.awt.event.{ComponentEvent, ComponentAdapter} -import scala.swing.{ComboBox, Button} -import scala.swing.event.{SelectionChanged, ButtonClicked} +import scala.swing.Button +import scala.swing.event.ButtonClicked import org.gjt.sp.jedit.{jEdit, View} @@ -46,18 +46,15 @@ }) private def handle_resize(): Unit = - GUI_Thread.require { pretty_text_area.zoom(zoom.factor) } + GUI_Thread.require { pretty_text_area.zoom(zoom) } /* controls */ - private val document_session: ComboBox[String] = { - new ComboBox(JEdit_Sessions.sessions_structure().build_topological_order.sorted) { + private val document_session = + new GUI.Selector(JEdit_Sessions.sessions_structure().build_topological_order.sorted) { val title = "Session" - listenTo(selection) - reactions += { case SelectionChanged(_) => } // FIXME } - } private val build_button = new Button("Build") { tooltip = "Build document" @@ -68,7 +65,7 @@ } } - private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() } + 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, diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/font_info.scala --- a/src/Tools/jEdit/src/font_info.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/font_info.scala Sat Aug 13 12:32:38 2022 +0200 @@ -78,9 +78,9 @@ } - /* zoom box */ + /* zoom */ - abstract class Zoom_Box extends GUI.Zoom_Box { tooltip = "Zoom factor for output font size" } + class Zoom extends GUI.Zoom { tooltip = "Zoom factor for output font size" } } sealed case class Font_Info(family: String, size: Float) { diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/info_dockable.scala --- a/src/Tools/jEdit/src/info_dockable.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/info_dockable.scala Sat Aug 13 12:32:38 2022 +0200 @@ -72,10 +72,10 @@ pretty_text_area.update(snapshot, results, info) - private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() } + 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.factor) } + GUI_Thread.require { pretty_text_area.zoom(zoom) } /* resize */ diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Sat Aug 13 12:32:38 2022 +0200 @@ -10,9 +10,6 @@ import isabelle._ -import scala.swing.ComboBox -import scala.swing.event.SelectionChanged - object JEdit_Sessions { /* session options */ @@ -88,9 +85,7 @@ (main_sessions.sorted ::: other_sessions.sorted).map(name => Logic_Entry(name = name)) } - val entries = default_entry :: session_entries - - new ComboBox[Logic_Entry](entries) with Option_Component { + new GUI.Selector[Logic_Entry](default_entry :: session_entries) with Option_Component { name = jedit_logic_option tooltip = "Logic session name (change requires restart)" val title = "Logic" @@ -102,12 +97,9 @@ } } def save(): Unit = options.string(jedit_logic_option) = selection.item.name + override def changed(): Unit = if (autosave) save() load() - if (autosave) { - listenTo(selection) - reactions += { case SelectionChanged(_) => save() } - } } } diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/jedit_spell_checker.scala --- a/src/Tools/jEdit/src/jedit_spell_checker.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Sat Aug 13 12:32:38 2022 +0200 @@ -10,7 +10,6 @@ import isabelle._ import javax.swing.JMenuItem -import scala.swing.ComboBox import org.gjt.sp.jedit.menu.EnhancedMenuItem import org.gjt.sp.jedit.jEdit @@ -86,9 +85,7 @@ val option_name = "spell_checker_dictionary" val opt = PIDE.options.value.check_name(option_name) - val entries = Spell_Checker.dictionaries - - new ComboBox[Spell_Checker.Dictionary](entries) with Option_Component { + new GUI.Selector[Spell_Checker.Dictionary](Spell_Checker.dictionaries) with Option_Component { name = option_name tooltip = GUI.tooltip_lines(opt.print_default) val title = opt.title() diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/monitor_dockable.scala --- a/src/Tools/jEdit/src/monitor_dockable.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/monitor_dockable.scala Sat Aug 13 12:32:38 2022 +0200 @@ -12,8 +12,8 @@ import java.awt.BorderLayout import scala.collection.immutable.Queue -import scala.swing.{TextField, ComboBox, Button} -import scala.swing.event.{SelectionChanged, ButtonClicked, ValueChanged} +import scala.swing.{TextField, Button} +import scala.swing.event.{ButtonClicked, ValueChanged} import org.jfree.chart.ChartPanel import org.jfree.data.xy.XYSeriesCollection @@ -64,10 +64,9 @@ /* controls */ - private val select_data = new ComboBox[String](ML_Statistics.all_fields.map(_._1)) { + private val select_data = new GUI.Selector[String](ML_Statistics.all_fields.map(_._1)) { tooltip = "Select visualized data collection" - listenTo(selection) - reactions += { case SelectionChanged(_) => data_name = selection.item; update_chart() } + override def changed(): Unit = { data_name = selection.item; update_chart() } } private val limit_data = new TextField("200", 5) { diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Sat Aug 13 12:32:38 2022 +0200 @@ -34,7 +34,7 @@ private def handle_resize(): Unit = - GUI_Thread.require { pretty_text_area.zoom(zoom.factor) } + GUI_Thread.require { pretty_text_area.zoom(zoom) } private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = { GUI_Thread.require {} @@ -93,7 +93,7 @@ reactions += { case ButtonClicked(_) => handle_update(true, None) } } - private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() } + private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } private val controls = Wrap_Panel( diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Aug 13 12:32:38 2022 +0200 @@ -122,8 +122,10 @@ refresh() } - def zoom(factor: Int): Unit = + def zoom(zoom: GUI.Zoom): Unit = { + val factor = if (zoom == null) 100 else zoom.factor resize(Font_Info.main(PIDE.options.real("jedit_font_scale") * factor / 100)) + } def update( base_snapshot: Document.Snapshot, diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/query_dockable.scala --- a/src/Tools/jEdit/src/query_dockable.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/query_dockable.scala Sat Aug 13 12:32:38 2022 +0200 @@ -31,7 +31,7 @@ class Query_Dockable(view: View, position: String) extends Dockable(view, position) { /* common GUI components */ - private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() } + private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } private def make_query( property: String, @@ -301,7 +301,7 @@ /* resize */ private def handle_resize(): Unit = - GUI_Thread.require { operations.foreach(_.pretty_text_area.zoom(zoom.factor)) } + GUI_Thread.require { operations.foreach(_.pretty_text_area.zoom(zoom)) } private val delay_resize = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/simplifier_trace_window.scala --- a/src/Tools/jEdit/src/simplifier_trace_window.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Sat Aug 13 12:32:38 2022 +0200 @@ -133,7 +133,7 @@ GUI_Thread.require {} private val pretty_text_area = new Pretty_Text_Area(view) - private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = do_paint() } + private val zoom = new Font_Info.Zoom { override def changed(): Unit = do_paint() } size = new Dimension(500, 500) contents = new BorderPanel { @@ -159,7 +159,7 @@ } def do_paint(): Unit = - GUI_Thread.later { pretty_text_area.zoom(zoom.factor) } + GUI_Thread.later { pretty_text_area.zoom(zoom) } def handle_resize(): Unit = do_paint() diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Sat Aug 13 12:32:38 2022 +0200 @@ -63,7 +63,7 @@ }) private def handle_resize(): Unit = - GUI_Thread.require { pretty_text_area.zoom(zoom.factor) } + GUI_Thread.require { pretty_text_area.zoom(zoom) } /* controls */ @@ -125,7 +125,7 @@ reactions += { case ButtonClicked(_) => sledgehammer.locate_query() } } - private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() } + private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } private val controls = Wrap_Panel( diff -r 7f6803788de3 -r 29441f2bfe81 src/Tools/jEdit/src/state_dockable.scala --- a/src/Tools/jEdit/src/state_dockable.scala Sat Aug 13 11:59:06 2022 +0200 +++ b/src/Tools/jEdit/src/state_dockable.scala Sat Aug 13 12:32:38 2022 +0200 @@ -46,7 +46,7 @@ }) private def handle_resize(): Unit = - GUI_Thread.require { pretty_text_area.zoom(zoom.factor) } + GUI_Thread.require { pretty_text_area.zoom(zoom) } /* update */ @@ -94,7 +94,7 @@ reactions += { case ButtonClicked(_) => print_state.locate_query() } } - private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() } + private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } private val controls = Wrap_Panel(