src/Tools/jEdit/src/jedit/plugin.scala
changeset 37164 8b4617ad1593
parent 37068 07936a4efe93
child 37177 17331ca75044
     1.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri May 28 16:01:25 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Fri May 28 17:48:18 2010 +0200
     1.3 @@ -71,6 +71,11 @@
     1.4        jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
     1.5    }
     1.6  
     1.7 +
     1.8 +  /* font */
     1.9 +
    1.10 +  def font_family(): String = jEdit.getProperty("view.font")
    1.11 +
    1.12    def font_size(): Float =
    1.13      (jEdit.getIntegerProperty("view.fontsize", 16) *
    1.14        Int_Property("relative-font-size", 100)).toFloat / 100