clarified module structure;
authorwenzelm
Sat Mar 01 19:55:01 2014 +0100 (2014-03-01)
changeset 558278a881f83e206
parent 55826 e56a52dd770a
child 55828 42ac3cfb89f6
clarified module structure;
src/Tools/jEdit/src/font_info.scala
src/Tools/jEdit/src/isabelle.scala
     1.1 --- a/src/Tools/jEdit/src/font_info.scala	Sat Mar 01 19:43:35 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/font_info.scala	Sat Mar 01 19:55:01 2014 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4 -/*  Title:      Tools/jEdit/src/jedit_font.scala
     1.5 +/*  Title:      Tools/jEdit/src/font_info.scala
     1.6      Author:     Makarius
     1.7  
     1.8 -Font information, derived from main view font.
     1.9 +Font information, derived from main jEdit view font.
    1.10  */
    1.11  
    1.12  package isabelle.jedit
    1.13 @@ -25,7 +25,7 @@
    1.14    def restrict_size(size: Float): Float = size max min_size min max_size
    1.15  
    1.16  
    1.17 -  /* jEdit font */
    1.18 +  /* main jEdit font */
    1.19  
    1.20    def main_family(): String = jEdit.getProperty("view.font")
    1.21  
    1.22 @@ -35,15 +35,54 @@
    1.23    def main(scale: Double = 1.0): Font_Info =
    1.24      Font_Info(main_family(), main_size(scale))
    1.25  
    1.26 -  def main_change(change: Float => Float)
    1.27 +
    1.28 +  /* incremental size change */
    1.29 +
    1.30 +  object main_change
    1.31    {
    1.32 -    val size0 = main_size()
    1.33 -    val size = restrict_size(change(size0)).round
    1.34 -    if (size != size0) {
    1.35 -      jEdit.setIntegerProperty("view.fontsize", size)
    1.36 -      jEdit.propertiesChanged()
    1.37 -      jEdit.saveSettings()
    1.38 -      jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
    1.39 +    private def change_size(change: Float => Float)
    1.40 +    {
    1.41 +      Swing_Thread.require()
    1.42 +
    1.43 +      val size0 = main_size()
    1.44 +      val size = restrict_size(change(size0)).round
    1.45 +      if (size != size0) {
    1.46 +        jEdit.setIntegerProperty("view.fontsize", size)
    1.47 +        jEdit.propertiesChanged()
    1.48 +        jEdit.saveSettings()
    1.49 +        jEdit.getActiveView().getStatus.setMessageAndClear("Text font size: " + size)
    1.50 +      }
    1.51 +    }
    1.52 +
    1.53 +    // owned by Swing thread
    1.54 +    private var steps = 0
    1.55 +    private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
    1.56 +    {
    1.57 +      change_size(size =>
    1.58 +        {
    1.59 +          var i = size.round
    1.60 +          while (steps != 0 && i > 0) {
    1.61 +            if (steps > 0)
    1.62 +              { i += (i / 10) max 1; steps -= 1 }
    1.63 +            else
    1.64 +              { i -= (i / 10) max 1; steps += 1 }
    1.65 +          }
    1.66 +          steps = 0
    1.67 +          i.toFloat
    1.68 +        })
    1.69 +    }
    1.70 +
    1.71 +    def step(i: Int)
    1.72 +    {
    1.73 +      steps += i
    1.74 +      delay.invoke()
    1.75 +    }
    1.76 +
    1.77 +    def reset(size: Float)
    1.78 +    {
    1.79 +      delay.revoke()
    1.80 +      steps = 0
    1.81 +      change_size(_ => size)
    1.82      }
    1.83    }
    1.84  }
     2.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 19:43:35 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sat Mar 01 19:55:01 2014 +0100
     2.3 @@ -186,37 +186,11 @@
     2.4  
     2.5    /* font size */
     2.6  
     2.7 -  private object font_size
     2.8 -  {
     2.9 -    // owned by Swing thread
    2.10 -    private var steps = 0
    2.11 -    private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
    2.12 -    {
    2.13 -      Font_Info.main_change(size =>
    2.14 -        {
    2.15 -          var i = size.round
    2.16 -          while (steps != 0 && i > 0) {
    2.17 -            if (steps > 0)
    2.18 -              { i += (i / 10) max 1; steps -= 1 }
    2.19 -            else
    2.20 -              { i -= (i / 10) max 1; steps += 1 }
    2.21 -          }
    2.22 -          steps = 0
    2.23 -          i.toFloat
    2.24 -        })
    2.25 -    }
    2.26 -    def step(i: Int) { steps += i; delay.invoke() }
    2.27 -    def reset() { delay.revoke(); steps = 0 }
    2.28 +  def reset_font_size() {
    2.29 +    Font_Info.main_change.reset(PIDE.options.int("jedit_reset_font_size").toFloat)
    2.30    }
    2.31 -
    2.32 -  def reset_font_size()
    2.33 -  {
    2.34 -    font_size.reset()
    2.35 -    Font_Info.main_change(_ => PIDE.options.int("jedit_reset_font_size").toFloat)
    2.36 -  }
    2.37 -
    2.38 -  def increase_font_size() { font_size.step(1) }
    2.39 -  def decrease_font_size() { font_size.step(-1) }
    2.40 +  def increase_font_size() { Font_Info.main_change.step(1) }
    2.41 +  def decrease_font_size() { Font_Info.main_change.step(-1) }
    2.42  
    2.43  
    2.44    /* structured edits */