src/Tools/jEdit/src/isabelle_actions.scala
changeset 50206 6626bc5ed053
parent 50205 788c8263e634
     1.1 --- a/src/Tools/jEdit/src/isabelle_actions.scala	Sun Nov 25 20:59:32 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle_actions.scala	Sun Nov 25 21:10:29 2012 +0100
     1.3 @@ -19,9 +19,8 @@
     1.4  
     1.5    def change_font_size(view: View, change: Int => Int)
     1.6    {
     1.7 -    val FONT_SIZE = "view.fontsize"
     1.8 -    val size = change(jEdit.getIntegerProperty(FONT_SIZE, 12)) max 5
     1.9 -    jEdit.setIntegerProperty(FONT_SIZE, size)
    1.10 +    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
    1.11 +    jEdit.setIntegerProperty("view.fontsize", size)
    1.12      jEdit.propertiesChanged()
    1.13      jEdit.saveSettings()
    1.14      view.getStatus.setMessageAndClear("Text font size: " + size)