equal
deleted
inserted
replaced
109 override def paintScreenLineRange(gfx: Graphics2D, |
109 override def paintScreenLineRange(gfx: Graphics2D, |
110 first_line: Int, last_line: Int, physical_lines: Array[Int], |
110 first_line: Int, last_line: Int, physical_lines: Array[Int], |
111 start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
111 start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
112 { |
112 { |
113 // no robust_body |
113 // no robust_body |
114 PIDE.editor.invoke() |
114 PIDE.editor.invoke_update() |
115 } |
115 } |
116 } |
116 } |
117 |
117 |
118 |
118 |
119 /* gutter */ |
119 /* gutter */ |