equal
deleted
inserted
replaced
163 private var highlight_range: Option[(Text.Range, Color)] = None |
163 private var highlight_range: Option[(Text.Range, Color)] = None |
164 |
164 |
165 |
165 |
166 /* CONTROL-mouse management */ |
166 /* CONTROL-mouse management */ |
167 |
167 |
|
168 private var control: Boolean = false |
|
169 |
168 private def exit_control() |
170 private def exit_control() |
169 { |
171 { |
170 exit_popup() |
172 exit_popup() |
171 highlight_range = None |
173 highlight_range = None |
172 } |
174 } |
182 override def windowDeactivated(e: WindowEvent) { exit_control() } |
184 override def windowDeactivated(e: WindowEvent) { exit_control() } |
183 } |
185 } |
184 |
186 |
185 private val mouse_motion_listener = new MouseMotionAdapter { |
187 private val mouse_motion_listener = new MouseMotionAdapter { |
186 override def mouseMoved(e: MouseEvent) { |
188 override def mouseMoved(e: MouseEvent) { |
187 val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown |
189 control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown |
188 val x = e.getX() |
190 val x = e.getX() |
189 val y = e.getY() |
191 val y = e.getY() |
190 |
192 |
191 if (!model.buffer.isLoaded) exit_control() |
193 if (!model.buffer.isLoaded) exit_control() |
192 else |
194 else |
286 override def getToolTipText(x: Int, y: Int): String = |
288 override def getToolTipText(x: Int, y: Int): String = |
287 { |
289 { |
288 Isabelle.swing_buffer_lock(model.buffer) { |
290 Isabelle.swing_buffer_lock(model.buffer) { |
289 val snapshot = model.snapshot() |
291 val snapshot = model.snapshot() |
290 val offset = text_area.xyToOffset(x, y) |
292 val offset = text_area.xyToOffset(x, y) |
291 snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match |
293 if (control) { |
292 { |
294 snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match |
293 case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text) |
295 { |
294 case _ => null |
296 case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text) |
|
297 case _ => null |
|
298 } |
|
299 } |
|
300 else { |
|
301 // FIXME snapshot.cumulate |
|
302 snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match |
|
303 { |
|
304 case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text) |
|
305 case _ => null |
|
306 } |
295 } |
307 } |
296 } |
308 } |
297 } |
309 } |
298 } |
310 } |
299 |
311 |