src/Tools/jEdit/src/isabelle.scala
changeset 53272 0dfd78ff7696
parent 53161 051cbf663b5f
child 53274 1760c01f1c78
equal deleted inserted replaced
53271:0460d6962ced 53272:0dfd78ff7696
    96   def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
    96   def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
    97 
    97 
    98 
    98 
    99   /* font size */
    99   /* font size */
   100 
   100 
   101   def change_font_size(view: View, change: Int => Int)
   101   def reset_font_size(view: View): Unit =
   102   {
   102     Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
   103     val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250
       
   104     jEdit.setIntegerProperty("view.fontsize", size)
       
   105     jEdit.propertiesChanged()
       
   106     jEdit.saveSettings()
       
   107     view.getStatus.setMessageAndClear("Text font size: " + size)
       
   108   }
       
   109 
   103 
   110   def reset_font_size(view: View): Unit =
   104   def increase_font_size(view: View): Unit =
   111     change_font_size(view, _ => PIDE.options.int("jedit_reset_font_size"))
   105     Rendering.font_size_change(view, i => i + ((i / 10) max 1))
   112   def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
   106 
   113   def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
   107   def decrease_font_size(view: View): Unit =
       
   108     Rendering.font_size_change(view, i => i - ((i / 10) max 1))
   114 
   109 
   115 
   110 
   116   /* structured insert */
   111   /* structured insert */
   117 
   112 
   118   def insert_line_padding(text_area: JEditTextArea, text: String)
   113   def insert_line_padding(text_area: JEditTextArea, text: String)