clarified signature: more explicit types;
more robust zoom.factor: work with uninitialized GUI components;
--- 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(