more uniform Font_Info.Zoom_Box;
authorwenzelm
Wed May 21 16:21:11 2014 +0200 (2014-05-21)
changeset 57044042d6e58cb40
parent 57043 0f44d6dbd2a4
child 57045 d2fb95869d55
more uniform Font_Info.Zoom_Box;
misc tuning and clarification;
src/Pure/GUI/gui.scala
src/Tools/Graphview/src/graph_panel.scala
src/Tools/Graphview/src/main_panel.scala
src/Tools/jEdit/src/font_info.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/query_dockable.scala
src/Tools/jEdit/src/simplifier_trace_window.scala
src/Tools/jEdit/src/sledgehammer_dockable.scala
     1.1 --- a/src/Pure/GUI/gui.scala	Wed May 21 15:24:42 2014 +0200
     1.2 +++ b/src/Pure/GUI/gui.scala	Wed May 21 16:21:11 2014 +0200
     1.3 @@ -117,19 +117,23 @@
     1.4  
     1.5    /* zoom box */
     1.6  
     1.7 -  class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
     1.8 +  private val Zoom_Factor = "([0-9]+)%?".r
     1.9 +
    1.10 +  abstract class Zoom_Box extends ComboBox[String](
    1.11      List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
    1.12    {
    1.13 -    val Factor = "([0-9]+)%?".r
    1.14 -    def parse(text: String): Int =
    1.15 +    def changed: Unit
    1.16 +    def factor: Int = parse(selection.item)
    1.17 +
    1.18 +    private def parse(text: String): Int =
    1.19        text match {
    1.20 -        case Factor(s) =>
    1.21 +        case Zoom_Factor(s) =>
    1.22            val i = Integer.parseInt(s)
    1.23            if (10 <= i && i < 1000) i else 100
    1.24          case _ => 100
    1.25        }
    1.26  
    1.27 -    def print(i: Int): String = i.toString + "%"
    1.28 +    private def print(i: Int): String = i.toString + "%"
    1.29  
    1.30      def set_item(i: Int) {
    1.31        peer.getEditor match {
    1.32 @@ -144,11 +148,10 @@
    1.33        case _ =>
    1.34      }
    1.35  
    1.36 -    reactions += {
    1.37 -      case SelectionChanged(_) => apply_factor(parse(selection.item))
    1.38 -    }
    1.39 +    selection.index = 3
    1.40 +
    1.41      listenTo(selection)
    1.42 -    selection.index = 3
    1.43 +    reactions += { case SelectionChanged(_) => changed }
    1.44    }
    1.45  
    1.46  
     2.1 --- a/src/Tools/Graphview/src/graph_panel.scala	Wed May 21 15:24:42 2014 +0200
     2.2 +++ b/src/Tools/Graphview/src/graph_panel.scala	Wed May 21 16:21:11 2014 +0200
     2.3 @@ -63,12 +63,12 @@
     2.4      refresh()
     2.5    }
     2.6  
     2.7 -  val zoom_box: GUI.Zoom_Box = new GUI.Zoom_Box(percent => rescale(0.01 * percent))
     2.8 +  val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) }
     2.9  
    2.10    def rescale(s: Double)
    2.11    {
    2.12      Transform.scale = s
    2.13 -    if (zoom_box != null) zoom_box.set_item((Transform.scale_discrete * 100).round.toInt)
    2.14 +    if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).round.toInt)
    2.15      refresh()
    2.16    }
    2.17  
     3.1 --- a/src/Tools/Graphview/src/main_panel.scala	Wed May 21 15:24:42 2014 +0200
     3.2 +++ b/src/Tools/Graphview/src/main_panel.scala	Wed May 21 16:21:11 2014 +0200
     3.3 @@ -67,7 +67,7 @@
     3.4        }
     3.5      }
     3.6      contents += Swing.RigidBox(new Dimension(10, 0))
     3.7 -    contents += graph_panel.zoom_box
     3.8 +    contents += graph_panel.zoom
     3.9  
    3.10      contents += Swing.RigidBox(new Dimension(10, 0))
    3.11      contents += new Button{
     4.1 --- a/src/Tools/jEdit/src/font_info.scala	Wed May 21 15:24:42 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/font_info.scala	Wed May 21 16:21:11 2014 +0200
     4.3 @@ -85,6 +85,11 @@
     4.4        change_size(_ => size)
     4.5      }
     4.6    }
     4.7 +
     4.8 +
     4.9 +  /* zoom box */
    4.10 +
    4.11 +  abstract class Zoom_Box extends GUI.Zoom_Box { tooltip = "Zoom factor for output font size" }
    4.12  }
    4.13  
    4.14  sealed case class Font_Info(family: String, size: Float)
     5.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Wed May 21 15:24:42 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Wed May 21 16:21:11 2014 +0200
     5.3 @@ -50,8 +50,6 @@
     5.4  {
     5.5    /* component state -- owned by Swing thread */
     5.6  
     5.7 -  private var zoom_factor = 100
     5.8 -
     5.9    private val snapshot = Info_Dockable.implicit_snapshot
    5.10    private val results = Info_Dockable.implicit_results
    5.11    private val info = Info_Dockable.implicit_info
    5.12 @@ -70,12 +68,14 @@
    5.13  
    5.14    pretty_text_area.update(snapshot, results, info)
    5.15  
    5.16 +  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
    5.17 +
    5.18    private def handle_resize()
    5.19    {
    5.20      Swing_Thread.require {}
    5.21  
    5.22      pretty_text_area.resize(
    5.23 -      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    5.24 +      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
    5.25    }
    5.26  
    5.27  
    5.28 @@ -88,9 +88,6 @@
    5.29      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
    5.30    })
    5.31  
    5.32 -  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
    5.33 -  zoom.tooltip = "Zoom factor for basic font size"
    5.34 -
    5.35    private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
    5.36      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
    5.37    add(controls.peer, BorderLayout.NORTH)
     6.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Wed May 21 15:24:42 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Wed May 21 16:21:11 2014 +0200
     6.3 @@ -22,7 +22,6 @@
     6.4  {
     6.5    /* component state -- owned by Swing thread */
     6.6  
     6.7 -  private var zoom_factor = 100
     6.8    private var do_update = true
     6.9    private var current_snapshot = Document.Snapshot.init
    6.10    private var current_command = Command.empty
    6.11 @@ -38,12 +37,14 @@
    6.12    override def detach_operation = pretty_text_area.detach_operation
    6.13  
    6.14  
    6.15 +  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
    6.16 +
    6.17    private def handle_resize()
    6.18    {
    6.19      Swing_Thread.require {}
    6.20  
    6.21      pretty_text_area.resize(
    6.22 -      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    6.23 +      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
    6.24    }
    6.25  
    6.26    private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
    6.27 @@ -126,10 +127,6 @@
    6.28  
    6.29    /* controls */
    6.30  
    6.31 -  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
    6.32 -    tooltip = "Zoom factor for output font size"
    6.33 -  }
    6.34 -
    6.35    private val auto_update = new CheckBox("Auto update") {
    6.36      tooltip = "Indicate automatic update following cursor movement"
    6.37      reactions += {
     7.1 --- a/src/Tools/jEdit/src/query_dockable.scala	Wed May 21 15:24:42 2014 +0200
     7.2 +++ b/src/Tools/jEdit/src/query_dockable.scala	Wed May 21 16:21:11 2014 +0200
     7.3 @@ -35,12 +35,7 @@
     7.4  {
     7.5    /* common GUI components */
     7.6  
     7.7 -  private var zoom_factor = 100
     7.8 -  private val zoom =
     7.9 -    new GUI.Zoom_Box(factor => if (zoom_factor != factor) { zoom_factor = factor; handle_resize() })
    7.10 -    {
    7.11 -      tooltip = "Zoom factor for output font size"
    7.12 -    }
    7.13 +  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
    7.14  
    7.15    private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
    7.16      new Completion_Popup.History_Text_Field(property)
    7.17 @@ -317,7 +312,7 @@
    7.18      Swing_Thread.require {
    7.19        for (op <- operations) {
    7.20          op.pretty_text_area.resize(
    7.21 -          Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    7.22 +          Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
    7.23        }
    7.24      }
    7.25  
     8.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 15:24:42 2014 +0200
     8.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 16:21:11 2014 +0200
     8.3 @@ -138,9 +138,8 @@
     8.4  {
     8.5    Swing_Thread.require {}
     8.6  
     8.7 -  private var zoom_factor = 100
     8.8 -
     8.9 -  val pretty_text_area = new Pretty_Text_Area(view)
    8.10 +  private val pretty_text_area = new Pretty_Text_Area(view)
    8.11 +  private val zoom = new Font_Info.Zoom_Box { def changed = do_paint() }
    8.12  
    8.13    size = new Dimension(500, 500)
    8.14    contents = new BorderPanel {
    8.15 @@ -170,7 +169,7 @@
    8.16    {
    8.17      Swing_Thread.later {
    8.18        pretty_text_area.resize(
    8.19 -        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    8.20 +        Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
    8.21      }
    8.22    }
    8.23  
    8.24 @@ -193,9 +192,6 @@
    8.25  
    8.26    /* controls */
    8.27  
    8.28 -  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
    8.29 -  zoom.tooltip = "Zoom factor for basic font size"
    8.30 -
    8.31    private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
    8.32      pretty_text_area.search_label,
    8.33      pretty_text_area.search_field,
     9.1 --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed May 21 15:24:42 2014 +0200
     9.2 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Wed May 21 16:21:11 2014 +0200
     9.3 @@ -51,14 +51,14 @@
     9.4  
     9.5    /* resize */
     9.6  
     9.7 -  private var zoom_factor = 100
     9.8 +  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
     9.9  
    9.10    private def handle_resize()
    9.11    {
    9.12      Swing_Thread.require {}
    9.13  
    9.14      pretty_text_area.resize(
    9.15 -      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    9.16 +      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
    9.17    }
    9.18  
    9.19    private val delay_resize =
    9.20 @@ -122,10 +122,6 @@
    9.21      reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
    9.22    }
    9.23  
    9.24 -  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
    9.25 -    tooltip = "Zoom factor for output font size"
    9.26 -  }
    9.27 -
    9.28    private val controls =
    9.29      new Wrap_Panel(Wrap_Panel.Alignment.Right)(
    9.30        provers_label, Component.wrap(provers), isar_proofs,