src/Tools/jEdit/src/isabelle.scala
changeset 53161 051cbf663b5f
parent 53021 d0fa3f446b9d
child 53272 0dfd78ff7696
     1.1 --- a/src/Tools/jEdit/src/isabelle.scala	Fri Aug 23 11:23:26 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Fri Aug 23 11:41:17 2013 +0200
     1.3 @@ -107,6 +107,8 @@
     1.4      view.getStatus.setMessageAndClear("Text font size: " + size)
     1.5    }
     1.6  
     1.7 +  def reset_font_size(view: View): Unit =
     1.8 +    change_font_size(view, _ => PIDE.options.int("jedit_reset_font_size"))
     1.9    def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
    1.10    def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
    1.11