src/Tools/jEdit/src/isabelle_actions.scala
changeset 50198 0c7b351a6871
parent 50187 b5a09812abc4
child 50205 788c8263e634
     1.1 --- a/src/Tools/jEdit/src/isabelle_actions.scala	Sun Nov 25 15:17:01 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle_actions.scala	Sun Nov 25 17:15:21 2012 +0100
     1.3 @@ -9,12 +9,28 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import org.gjt.sp.jedit.Buffer
     1.8 +import org.gjt.sp.jedit.{jEdit, View, Buffer}
     1.9  import org.gjt.sp.jedit.textarea.JEditTextArea
    1.10  
    1.11  
    1.12  object Isabelle_Actions
    1.13  {
    1.14 +  /* font size */
    1.15 +
    1.16 +  def change_font_size(view: View, change: Int => Int)
    1.17 +  {
    1.18 +    val FONT_SIZE = "view.fontsize"
    1.19 +    val size = change(jEdit.getIntegerProperty(FONT_SIZE, 12)) max 5
    1.20 +    jEdit.setIntegerProperty(FONT_SIZE, size)
    1.21 +    jEdit.propertiesChanged()
    1.22 +    jEdit.saveSettings()
    1.23 +    view.getStatus.setMessageAndClear("Text font size: " + size)
    1.24 +  }
    1.25 +
    1.26 +  def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
    1.27 +  def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
    1.28 +
    1.29 +
    1.30    /* full checking */
    1.31  
    1.32    def check_buffer(buffer: Buffer)