27 |
27 |
28 |
28 |
29 class Rich_Text_Area( |
29 class Rich_Text_Area( |
30 view: View, |
30 view: View, |
31 text_area: TextArea, |
31 text_area: TextArea, |
32 get_rendering: () => Rendering, |
32 get_rendering: () => JEdit_Rendering, |
33 close_action: () => Unit, |
33 close_action: () => Unit, |
34 get_search_pattern: () => Option[Regex], |
34 get_search_pattern: () => Option[Regex], |
35 caret_update: () => Unit, |
35 caret_update: () => Unit, |
36 caret_visible: Boolean, |
36 caret_visible: Boolean, |
37 enable_hovering: Boolean) |
37 enable_hovering: Boolean) |
70 pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText") |
70 pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText") |
71 |
71 |
72 |
72 |
73 /* common painter state */ |
73 /* common painter state */ |
74 |
74 |
75 @volatile private var painter_rendering: Rendering = null |
75 @volatile private var painter_rendering: JEdit_Rendering = null |
76 @volatile private var painter_clip: Shape = null |
76 @volatile private var painter_clip: Shape = null |
77 @volatile private var caret_focus: Set[Long] = Set.empty |
77 @volatile private var caret_focus: Set[Long] = Set.empty |
78 |
78 |
79 private val set_state = new TextAreaExtension |
79 private val set_state = new TextAreaExtension |
80 { |
80 { |
103 painter_clip = null |
103 painter_clip = null |
104 caret_focus = Set.empty |
104 caret_focus = Set.empty |
105 } |
105 } |
106 } |
106 } |
107 |
107 |
108 def robust_rendering(body: Rendering => Unit) |
108 def robust_rendering(body: JEdit_Rendering => Unit) |
109 { |
109 { |
110 robust_body(()) { body(painter_rendering) } |
110 robust_body(()) { body(painter_rendering) } |
111 } |
111 } |
112 |
112 |
113 |
113 |
114 /* active areas within the text */ |
114 /* active areas within the text */ |
115 |
115 |
116 private class Active_Area[A]( |
116 private class Active_Area[A]( |
117 rendering: Rendering => Text.Range => Option[Text.Info[A]], |
117 rendering: JEdit_Rendering => Text.Range => Option[Text.Info[A]], |
118 cursor: Option[Int]) |
118 cursor: Option[Int]) |
119 { |
119 { |
120 private var the_text_info: Option[(String, Text.Info[A])] = None |
120 private var the_text_info: Option[(String, Text.Info[A])] = None |
121 |
121 |
122 def is_active: Boolean = the_text_info.isDefined |
122 def is_active: Boolean = the_text_info.isDefined |
145 } JEdit_Lib.invalidate_range(text_area, r2) |
145 } JEdit_Lib.invalidate_range(text_area, r2) |
146 the_text_info = new_text_info |
146 the_text_info = new_text_info |
147 } |
147 } |
148 } |
148 } |
149 |
149 |
150 def update_rendering(r: Rendering, range: Text.Range) |
150 def update_rendering(r: JEdit_Rendering, range: Text.Range) |
151 { update(rendering(r)(range)) } |
151 { update(rendering(r)(range)) } |
152 |
152 |
153 def reset { update(None) } |
153 def reset { update(None) } |
154 } |
154 } |
155 |
155 |
156 // owned by GUI thread |
156 // owned by GUI thread |
157 |
157 |
158 private val highlight_area = |
158 private val highlight_area = |
159 new Active_Area[Color]( |
159 new Active_Area[Color]( |
160 (rendering: Rendering) => rendering.highlight _, None) |
160 (rendering: JEdit_Rendering) => rendering.highlight _, None) |
161 |
161 |
162 private val hyperlink_area = |
162 private val hyperlink_area = |
163 new Active_Area[PIDE.editor.Hyperlink]( |
163 new Active_Area[PIDE.editor.Hyperlink]( |
164 (rendering: Rendering) => rendering.hyperlink _, Some(Cursor.HAND_CURSOR)) |
164 (rendering: JEdit_Rendering) => rendering.hyperlink _, Some(Cursor.HAND_CURSOR)) |
165 |
165 |
166 private val active_area = |
166 private val active_area = |
167 new Active_Area[XML.Elem]( |
167 new Active_Area[XML.Elem]( |
168 (rendering: Rendering) => rendering.active _, Some(Cursor.DEFAULT_CURSOR)) |
168 (rendering: JEdit_Rendering) => rendering.active _, Some(Cursor.DEFAULT_CURSOR)) |
169 |
169 |
170 private val active_areas = |
170 private val active_areas = |
171 List((highlight_area, true), (hyperlink_area, true), (active_area, false)) |
171 List((highlight_area, true), (hyperlink_area, true), (active_area, false)) |
172 def active_reset(): Unit = active_areas.foreach(_._1.reset) |
172 def active_reset(): Unit = active_areas.foreach(_._1.reset) |
173 |
173 |
360 /* text */ |
360 /* text */ |
361 |
361 |
362 private def caret_enabled: Boolean = |
362 private def caret_enabled: Boolean = |
363 caret_visible && (!text_area.hasFocus || text_area.isCaretVisible) |
363 caret_visible && (!text_area.hasFocus || text_area.isCaretVisible) |
364 |
364 |
365 private def caret_color(rendering: Rendering, offset: Text.Offset): Color = |
365 private def caret_color(rendering: JEdit_Rendering, offset: Text.Offset): Color = |
366 { |
366 { |
367 if (text_area.isCaretVisible) text_area.getPainter.getCaretColor |
367 if (text_area.isCaretVisible) text_area.getPainter.getCaretColor |
368 else { |
368 else { |
369 val debug_positions = |
369 val debug_positions = |
370 (for { |
370 (for { |
375 rendering.caret_debugger_color |
375 rendering.caret_debugger_color |
376 else rendering.caret_invisible_color |
376 else rendering.caret_invisible_color |
377 } |
377 } |
378 } |
378 } |
379 |
379 |
380 private def paint_chunk_list(rendering: Rendering, |
380 private def paint_chunk_list(rendering: JEdit_Rendering, |
381 gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float = |
381 gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float = |
382 { |
382 { |
383 val clip_rect = gfx.getClipBounds |
383 val clip_rect = gfx.getClipBounds |
384 val painter = text_area.getPainter |
384 val painter = text_area.getPainter |
385 val font_context = painter.getFontRenderContext |
385 val font_context = painter.getFontRenderContext |