src/Tools/jEdit/src/rendering.scala
changeset 50206 6626bc5ed053
parent 50205 788c8263e634
child 50215 97959912840a
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Nov 25 20:59:32 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Nov 25 21:10:29 2012 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  import javax.swing.Icon
     1.5  
     1.6  import org.gjt.sp.jedit.syntax.{Token => JEditToken}
     1.7 -import org.gjt.sp.jedit.GUIUtilities
     1.8 +import org.gjt.sp.jedit.{jEdit, GUIUtilities}
     1.9  
    1.10  import scala.collection.immutable.SortedMap
    1.11  
    1.12 @@ -58,6 +58,14 @@
    1.13    val tooltip_detach_icon = load_icon("16x16/actions/window-new.png")
    1.14  
    1.15  
    1.16 +  /* jEdit font */
    1.17 +
    1.18 +  def font_family(): String = jEdit.getProperty("view.font")
    1.19 +
    1.20 +  def font_size(scale: String): Float =
    1.21 +    (jEdit.getIntegerProperty("view.fontsize", 16) * PIDE.options.real(scale)).toFloat
    1.22 +
    1.23 +
    1.24    /* token markup -- text styles */
    1.25  
    1.26    private val command_style: Map[String, Byte] =