8 package isabelle.jedit |
8 package isabelle.jedit |
9 |
9 |
10 |
10 |
11 import isabelle._ |
11 import isabelle._ |
12 |
12 |
13 import java.awt.{Graphics2D, Shape, Color, Point, Toolkit} |
13 import java.awt.{Graphics2D, Shape, Color, Point, Toolkit, Cursor} |
14 import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent, |
14 import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent, |
15 FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} |
15 FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} |
16 import java.awt.font.TextAttribute |
16 import java.awt.font.TextAttribute |
17 import java.text.AttributedString |
17 import java.text.AttributedString |
18 import java.util.ArrayList |
18 import java.util.ArrayList |
98 } |
98 } |
99 |
99 |
100 |
100 |
101 /* active areas within the text */ |
101 /* active areas within the text */ |
102 |
102 |
103 private class Active_Area[A](rendering: Rendering => Text.Range => Option[Text.Info[A]]) |
103 private class Active_Area[A]( |
|
104 rendering: Rendering => Text.Range => Option[Text.Info[A]], |
|
105 cursor: Option[Int]) |
104 { |
106 { |
105 private var the_text_info: Option[(String, Text.Info[A])] = None |
107 private var the_text_info: Option[(String, Text.Info[A])] = None |
106 |
108 |
107 def is_active: Boolean = the_text_info.isDefined |
109 def is_active: Boolean = the_text_info.isDefined |
108 def text_info: Option[(String, Text.Info[A])] = the_text_info |
110 def text_info: Option[(String, Text.Info[A])] = the_text_info |
113 val old_text_info = the_text_info |
115 val old_text_info = the_text_info |
114 val new_text_info = |
116 val new_text_info = |
115 new_info.map(info => (text_area.getText(info.range.start, info.range.length), info)) |
117 new_info.map(info => (text_area.getText(info.range.start, info.range.length), info)) |
116 |
118 |
117 if (new_text_info != old_text_info) { |
119 if (new_text_info != old_text_info) { |
|
120 if (cursor.isDefined) { |
|
121 if (new_text_info.isDefined) |
|
122 text_area.getPainter.setCursor(Cursor.getPredefinedCursor(cursor.get)) |
|
123 else |
|
124 text_area.getPainter.resetCursor |
|
125 } |
118 for { |
126 for { |
119 r0 <- JEdit_Lib.visible_range(text_area) |
127 r0 <- JEdit_Lib.visible_range(text_area) |
120 opt <- List(old_text_info, new_text_info) |
128 opt <- List(old_text_info, new_text_info) |
121 (_, Text.Info(r1, _)) <- opt |
129 (_, Text.Info(r1, _)) <- opt |
122 r2 <- r1.try_restrict(r0) // FIXME more precise?! |
130 r2 <- r1.try_restrict(r0) // FIXME more precise?! |
131 def reset { update(None) } |
139 def reset { update(None) } |
132 } |
140 } |
133 |
141 |
134 // owned by Swing thread |
142 // owned by Swing thread |
135 |
143 |
136 private val highlight_area = new Active_Area[Color]((r: Rendering) => r.highlight _) |
144 private val highlight_area = |
|
145 new Active_Area[Color]((r: Rendering) => r.highlight _, None) |
137 private val hyperlink_area = |
146 private val hyperlink_area = |
138 new Active_Area[PIDE.editor.Hyperlink]((r: Rendering) => r.hyperlink _) |
147 new Active_Area[PIDE.editor.Hyperlink]( |
139 private val active_area = new Active_Area[XML.Elem]((r: Rendering) => r.active _) |
148 (r: Rendering) => r.hyperlink _, Some(Cursor.HAND_CURSOR)) |
|
149 private val active_area = |
|
150 new Active_Area[XML.Elem]((r: Rendering) => r.active _, Some(Cursor.DEFAULT_CURSOR)) |
140 |
151 |
141 private val active_areas = |
152 private val active_areas = |
142 List((highlight_area, true), (hyperlink_area, true), (active_area, false)) |
153 List((highlight_area, true), (hyperlink_area, true), (active_area, false)) |
143 def active_reset(): Unit = active_areas.foreach(_._1.reset) |
154 def active_reset(): Unit = active_areas.foreach(_._1.reset) |
144 |
155 |