equal
deleted
inserted
replaced
56 /* font */ |
56 /* font */ |
57 |
57 |
58 def font_family(): String = jEdit.getProperty("view.font") |
58 def font_family(): String = jEdit.getProperty("view.font") |
59 |
59 |
60 def font_size(): Float = |
60 def font_size(): Float = |
61 (jEdit.getIntegerProperty("view.fontsize", 16) * |
61 (jEdit.getIntegerProperty("view.fontsize", 16) * options.real("jedit_font_scale")).toFloat |
62 options.int("jedit_relative_font_size")).toFloat / 100 |
|
63 |
62 |
64 |
63 |
65 /* tooltip markup */ |
64 /* tooltip markup */ |
66 |
65 |
67 def tooltip(text: String): String = |
66 def tooltip(text: String): String = |