equal
deleted
inserted
replaced
101 def font_family(): String = jEdit.getProperty("view.font") |
101 def font_family(): String = jEdit.getProperty("view.font") |
102 |
102 |
103 def font_size(): Float = |
103 def font_size(): Float = |
104 (jEdit.getIntegerProperty("view.fontsize", 16) * |
104 (jEdit.getIntegerProperty("view.fontsize", 16) * |
105 Int_Property("relative-font-size", 100)).toFloat / 100 |
105 Int_Property("relative-font-size", 100)).toFloat / 100 |
106 |
|
107 |
|
108 /* text area ranges */ |
|
109 |
|
110 sealed case class Gfx_Range(val x: Int, val y: Int, val length: Int) |
|
111 |
|
112 def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = |
|
113 { |
|
114 val p = text_area.offsetToXY(range.start) |
|
115 val q = text_area.offsetToXY(range.stop) |
|
116 if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x)) |
|
117 else None |
|
118 } |
|
119 |
106 |
120 |
107 |
121 /* tooltip markup */ |
108 /* tooltip markup */ |
122 |
109 |
123 def tooltip(text: String): String = |
110 def tooltip(text: String): String = |