src/Tools/jEdit/src/rendering.scala
changeset 53230 6589ff56cc3c
parent 52980 28f59ca8ce78
child 53272 0dfd78ff7696
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Aug 27 15:35:51 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Aug 27 16:09:28 2013 +0200
     1.3 @@ -49,6 +49,11 @@
     1.4      (jEdit.getIntegerProperty("view.fontsize", 16) * PIDE.options.real(scale)).toFloat
     1.5  
     1.6  
     1.7 +  /* popup window bounds */
     1.8 +
     1.9 +  def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
    1.10 +
    1.11 +
    1.12    /* token markup -- text styles */
    1.13  
    1.14    private val command_style: Map[String, Byte] =
    1.15 @@ -372,7 +377,6 @@
    1.16    }
    1.17  
    1.18    val tooltip_margin: Int = options.int("jedit_tooltip_margin")
    1.19 -  val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8
    1.20  
    1.21    lazy val tooltip_close_icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
    1.22    lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))