equal
deleted
inserted
replaced
98 override def paintScreenLineRange(gfx: Graphics2D, |
98 override def paintScreenLineRange(gfx: Graphics2D, |
99 first_line: Int, last_line: Int, physical_lines: Array[Int], |
99 first_line: Int, last_line: Int, physical_lines: Array[Int], |
100 start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
100 start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
101 { |
101 { |
102 // no robust_body |
102 // no robust_body |
103 model.update_perspective() |
103 model.flush() |
104 } |
104 } |
105 } |
105 } |
106 |
106 |
107 |
107 |
108 /* gutter */ |
108 /* gutter */ |