clarified signature: more explicit types;
authorwenzelm
Sat, 13 Aug 2022 12:32:38 +0200
changeset 75839 29441f2bfe81
parent 75838 7f6803788de3
child 75840 f8c412a45af8
clarified signature: more explicit types; more robust zoom.factor: work with uninitialized GUI components;
src/Pure/GUI/gui.scala
src/Tools/Graphview/graph_panel.scala
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/document_dockable.scala
src/Tools/jEdit/src/font_info.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/jedit_sessions.scala
src/Tools/jEdit/src/jedit_spell_checker.scala
src/Tools/jEdit/src/monitor_dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/query_dockable.scala
src/Tools/jEdit/src/simplifier_trace_window.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
src/Tools/jEdit/src/state_dockable.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() }
   }
 
 
--- 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() }
--- 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(
--- 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("<html><b>Build</b></html>") {
       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,
--- 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) {
--- 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 */
--- 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() }
-      }
     }
   }
 
--- 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()
--- 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) {
--- 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(
--- 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,
--- 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() }
--- 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()
 
--- 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(
--- 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(