src/Tools/jEdit/src/rendering.scala
changeset 55823 0331b6d2ab0c
parent 55820 61869776ce1f
child 55824 22bc50a19afa
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 15:58:47 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 01 16:34:30 2014 +0100
     1.3 @@ -54,11 +54,14 @@
     1.4  
     1.5    def font_size_change(view: View, change: Int => Int)
     1.6    {
     1.7 -    val size = change(view_font_size()) max font_size0 min font_size1
     1.8 -    jEdit.setIntegerProperty("view.fontsize", size)
     1.9 -    jEdit.propertiesChanged()
    1.10 -    jEdit.saveSettings()
    1.11 -    view.getStatus.setMessageAndClear("Text font size: " + size)
    1.12 +    val size0 = view_font_size()
    1.13 +    val size = change(size0) max font_size0 min font_size1
    1.14 +    if (size != size0) {
    1.15 +      jEdit.setIntegerProperty("view.fontsize", size)
    1.16 +      jEdit.propertiesChanged()
    1.17 +      jEdit.saveSettings()
    1.18 +      view.getStatus.setMessageAndClear("Text font size: " + size)
    1.19 +    }
    1.20    }
    1.21  
    1.22