src/Tools/jEdit/src/isabelle.scala
changeset 50775 8c1cda8ad833
parent 50433 9131dadb2bf7
child 51533 3f6280aedbcc
equal deleted inserted replaced
50774:ac53370dfae1 50775:8c1cda8ad833
    53 
    53 
    54   /* font size */
    54   /* font size */
    55 
    55 
    56   def change_font_size(view: View, change: Int => Int)
    56   def change_font_size(view: View, change: Int => Int)
    57   {
    57   {
    58     val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
    58     val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250
    59     jEdit.setIntegerProperty("view.fontsize", size)
    59     jEdit.setIntegerProperty("view.fontsize", size)
    60     jEdit.propertiesChanged()
    60     jEdit.propertiesChanged()
    61     jEdit.saveSettings()
    61     jEdit.saveSettings()
    62     view.getStatus.setMessageAndClear("Text font size: " + size)
    62     view.getStatus.setMessageAndClear("Text font size: " + size)
    63   }
    63   }