src/Tools/jEdit/src/rendering.scala
changeset 50554 0493efcc97e9
parent 50547 ebd75dfaab73
child 50643 09394eaf6804
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 20:05:53 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 21:07:52 2012 +0100
     1.3 @@ -346,6 +346,9 @@
     1.4      Library.separate(Pretty.FBreak, all_tips.toList)
     1.5    }
     1.6  
     1.7 +  val tooltip_margin: Int = options.int("jedit_tooltip_margin")
     1.8 +  val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8
     1.9 +
    1.10  
    1.11    def gutter_message(range: Text.Range): Option[Icon] =
    1.12    {