# HG changeset patch # User wenzelm # Date 1347637039 -7200 # Node ID 34ac36642a3136833acf18d2f784c5e9df18ae01 # Parent 6e0c0ffb6ec7b75fdc88b2c9223127d933a93a01 more general Document_Model.point_range; more general Document_View.Active_Area; eliminated dead popup material; diff -r 6e0c0ffb6ec7 -r 34ac36642a31 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Fri Sep 14 13:52:16 2012 +0200 +++ b/src/Tools/jEdit/src/document_model.scala Fri Sep 14 17:37:19 2012 +0200 @@ -92,6 +92,24 @@ } + + /* point range */ + + def point_range(offset: Text.Offset): Text.Range = + Isabelle.buffer_lock(buffer) { + def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0) + try { + val c = text(offset) + if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1))) + Text.Range(offset, offset + 2) + else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1))) + Text.Range(offset - 1, offset + 1) + else Text.Range(offset, offset + 1) + } + catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } + } + + /* pending text edits */ private object pending_edits // owned by Swing thread diff -r 6e0c0ffb6ec7 -r 34ac36642a31 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Fri Sep 14 13:52:16 2012 +0200 +++ b/src/Tools/jEdit/src/document_view.scala Fri Sep 14 17:37:19 2012 +0200 @@ -19,7 +19,6 @@ import java.awt.{Color, Graphics2D, Point} import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent, FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} -import javax.swing.{Popup, PopupFactory, SwingUtilities, BorderFactory} import javax.swing.event.{CaretListener, CaretEvent} import org.gjt.sp.util.Log @@ -143,77 +142,56 @@ } - /* HTML popups */ + /* active areas within the text */ - private var html_popup: Option[Popup] = None + private class Active_Area[A]( + rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]]) + { + private var the_info: Option[Text.Info[A]] = None - private def exit_popup() { html_popup.map(_.hide) } + def info: Option[Text.Info[A]] = the_info - private val html_panel = - new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size())) - html_panel.setBorder(BorderFactory.createLineBorder(Color.black)) + def update(new_info: Option[Text.Info[A]]) + { + val old_info = the_info + if (new_info != old_info) { + for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt } + invalidate_range(range) + the_info = new_info + } + } - private def html_panel_resize() - { - Swing_Thread.now { - html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size())) - } + def update_rendering(r: Isabelle_Rendering, range: Text.Range) + { update(rendering(r)(range)) } + + def reset { update(None) } } - private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int) - { - exit_popup() -/* FIXME broken - val offset = text_area.xyToOffset(x, y) - val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter) - - // FIXME snapshot.cumulate - snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Rendering.popup) match { - case Text.Info(_, Some(msg)) #:: _ => - val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60) - html_panel.render_sync(List(msg)) - Thread.sleep(10) // FIXME !? - popup.show - html_popup = Some(popup) - case _ => - } -*/ - } - - - /* subexpression highlighting and hyperlinks */ - - @volatile private var _highlight_range: Option[Text.Info[Color]] = None - def highlight_range(): Option[Text.Info[Color]] = _highlight_range - - @volatile private var _hyperlink_range: Option[Text.Info[Hyperlink]] = None - def hyperlink_range(): Option[Text.Info[Hyperlink]] = _hyperlink_range + // owned by Swing thread private var control: Boolean = false - private def exit_control() - { - exit_popup() - _highlight_range = None - _hyperlink_range = None - } + private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.subexp _) + def highlight_info(): Option[Text.Info[Color]] = highlight_area.info + + private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _) + def hyperlink_info(): Option[Text.Info[Hyperlink]] = hyperlink_area.info + + private val active_areas = List(highlight_area, hyperlink_area) + private def active_reset(): Unit = active_areas.foreach(_.reset) private val focus_listener = new FocusAdapter { - override def focusLost(e: FocusEvent) { - // FIXME exit_control !? - _highlight_range = None - _hyperlink_range = None - } + override def focusLost(e: FocusEvent) { active_reset() } } private val window_listener = new WindowAdapter { - override def windowIconified(e: WindowEvent) { exit_control() } - override def windowDeactivated(e: WindowEvent) { exit_control() } + override def windowIconified(e: WindowEvent) { active_reset() } + override def windowDeactivated(e: WindowEvent) { active_reset() } } private val mouse_listener = new MouseAdapter { override def mouseClicked(e: MouseEvent) { - hyperlink_range match { + hyperlink_area.info match { case Some(Text.Info(range, link)) => link.follow(text_area.getView) case None => } @@ -222,37 +200,15 @@ private val mouse_motion_listener = new MouseMotionAdapter { override def mouseMoved(e: MouseEvent) { - Swing_Thread.assert() - control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown - val x = e.getX() - val y = e.getY() - - if (!model.buffer.isLoaded) exit_control() - else + if (control && model.buffer.isLoaded) { Isabelle.buffer_lock(model.buffer) { - val snapshot = model.snapshot() - val rendering = Isabelle_Rendering(snapshot, Isabelle.options.value) - - if (control) init_popup(snapshot, x, y) - - def update_range[A]( - rendering: Text.Range => Option[Text.Info[A]], - info: Option[Text.Info[A]]): Option[Text.Info[A]] = - { - for (Text.Info(range, _) <- info) invalidate_range(range) - val new_info = - if (control) { - val offset = text_area.xyToOffset(x, y) - rendering(Text.Range(offset, offset + 1)) - } - else None - for (Text.Info(range, _) <- info) invalidate_range(range) - new_info - } - _highlight_range = update_range(rendering.subexp, _highlight_range) - _hyperlink_range = update_range(rendering.hyperlink, _hyperlink_range) + val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value) + val mouse_range = model.point_range(text_area.xyToOffset(e.getX(), e.getY())) + active_areas.foreach(_.update_rendering(rendering, mouse_range)) } + } + else active_reset() } } @@ -316,24 +272,6 @@ } - /* caret range */ - - def caret_range(): Text.Range = - Isabelle.buffer_lock(model.buffer) { - def text(i: Text.Offset): Char = model.buffer.getText(i, 1).charAt(0) - val caret = text_area.getCaretPosition - try { - val c = text(caret) - if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(caret + 1))) - Text.Range(caret, caret + 2) - else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(caret - 1))) - Text.Range(caret - 1, caret + 1) - else Text.Range(caret, caret + 1) - } - catch { case _: ArrayIndexOutOfBoundsException => Text.Range(caret, caret + 1) } - } - - /* caret handling */ def selected_command(): Option[Command] = @@ -408,8 +346,6 @@ } } - case Session.Global_Settings => html_panel_resize() - case bad => System.err.println("command_change_actor: ignoring bad message " + bad) } } @@ -452,6 +388,5 @@ text_area_painter.deactivate() painter.removeExtension(tooltip_painter) painter.removeExtension(update_perspective) - exit_popup() } } diff -r 6e0c0ffb6ec7 -r 34ac36642a31 src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala Fri Sep 14 13:52:16 2012 +0200 +++ b/src/Tools/jEdit/src/text_area_painter.scala Fri Sep 14 17:37:19 2012 +0200 @@ -185,7 +185,7 @@ else chunk_font.getStringBounds(s, font_context).getWidth.toFloat val caret_range = - if (text_area.isCaretVisible) doc_view.caret_range() + if (text_area.isCaretVisible) model.point_range(text_area.getCaretPosition) else Text.Range(-1) val markup = @@ -296,9 +296,9 @@ gfx.fillRect(r.x, y + i * line_height, r.length, line_height) } - // highlighted range -- potentially from other snapshot + // highlight range -- potentially from other snapshot for { - info <- doc_view.highlight_range() + info <- doc_view.highlight_info() Text.Info(range, color) <- info.try_restrict(line_range) r <- gfx_range(range) } { @@ -308,7 +308,7 @@ // hyperlink range -- potentially from other snapshot for { - info <- doc_view.hyperlink_range() + info <- doc_view.hyperlink_info() Text.Info(range, _) <- info.try_restrict(line_range) r <- gfx_range(range) } {