src/Tools/jEdit/src/isabelle.scala
changeset 53272 0dfd78ff7696
parent 53161 051cbf663b5f
child 53274 1760c01f1c78
     1.1 --- a/src/Tools/jEdit/src/isabelle.scala	Thu Aug 29 09:16:03 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Thu Aug 29 10:01:59 2013 +0200
     1.3 @@ -98,19 +98,14 @@
     1.4  
     1.5    /* font size */
     1.6  
     1.7 -  def change_font_size(view: View, change: Int => Int)
     1.8 -  {
     1.9 -    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250
    1.10 -    jEdit.setIntegerProperty("view.fontsize", size)
    1.11 -    jEdit.propertiesChanged()
    1.12 -    jEdit.saveSettings()
    1.13 -    view.getStatus.setMessageAndClear("Text font size: " + size)
    1.14 -  }
    1.15 +  def reset_font_size(view: View): Unit =
    1.16 +    Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
    1.17  
    1.18 -  def reset_font_size(view: View): Unit =
    1.19 -    change_font_size(view, _ => PIDE.options.int("jedit_reset_font_size"))
    1.20 -  def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
    1.21 -  def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
    1.22 +  def increase_font_size(view: View): Unit =
    1.23 +    Rendering.font_size_change(view, i => i + ((i / 10) max 1))
    1.24 +
    1.25 +  def decrease_font_size(view: View): Unit =
    1.26 +    Rendering.font_size_change(view, i => i - ((i / 10) max 1))
    1.27  
    1.28  
    1.29    /* structured insert */