# HG changeset patch # User wenzelm # Date 1285707725 -7200 # Node ID 0294948ba9622209e1812d38991a54f9406fb5d6 # Parent c7f0fa0593f0796f2d6a094df5389ef1045fa29b basic support for message popups via HTML_Panel; more systematic CONTROL-mouse management; tuned; diff -r c7f0fa0593f0 -r 0294948ba962 src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Tue Sep 28 20:49:39 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Tue Sep 28 23:02:05 2010 +0200 @@ -12,9 +12,9 @@ import scala.actors.Actor._ +import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point} import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent} -import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D} -import javax.swing.{JPanel, ToolTipManager} +import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities} import javax.swing.event.{CaretListener, CaretEvent} import org.gjt.sp.jedit.{jEdit, OperatingSystem} @@ -109,39 +109,37 @@ } - /* commands_changed_actor */ + /* HTML popups */ + + private var html_popup: Option[Popup] = None - private val commands_changed_actor = actor { - loop { - react { - case Session.Commands_Changed(changed) => - val buffer = model.buffer - Isabelle.swing_buffer_lock(buffer) { - val snapshot = model.snapshot() + private def exit_popup() { html_popup.map(_.hide) } - if (changed.exists(snapshot.node.commands.contains)) - overview.repaint() + private val html_panel = + new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size())) { + } - val visible_range = screen_lines_range() - val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1) - if (visible_cmds.exists(changed)) { - for { - line <- 0 until text_area.getVisibleLines - val start = text_area.getScreenLineStartOffset(line) if start >= 0 - val end = text_area.getScreenLineEndOffset(line) if end >= 0 - val range = proper_line_range(start, end) - val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1) - if line_cmds.exists(changed) - } text_area.invalidateScreenLineRange(line, line) + private def html_panel_resize() + { + Swing_Thread.now { + html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size())) + } + } - // FIXME danger of deadlock!? - // FIXME potentially slow!? - model.buffer.propertiesChanged() - } - } + private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int) + { + exit_popup() + val offset = text_area.xyToOffset(x, y) + val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter) - case bad => System.err.println("command_change_actor: ignoring bad message " + bad) - } + // FIXME snapshot.cumulate + snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.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)) + popup.show + html_popup = Some(popup) + case _ => } } @@ -160,19 +158,34 @@ private var highlight_range: Option[(Text.Range, Color)] = None + + /* CONTROL-mouse management */ + + private def exit_control() + { + exit_popup() + highlight_range = None + } + private val focus_listener = new FocusAdapter { - override def focusLost(e: FocusEvent) { highlight_range = None } + override def focusLost(e: FocusEvent) { exit_control() } } private val mouse_motion_listener = new MouseMotionAdapter { override def mouseMoved(e: MouseEvent) { val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown - if (!model.buffer.isLoaded) highlight_range = None + val x = e.getX() + val y = e.getY() + + if (!model.buffer.isLoaded) exit_control() else Isabelle.swing_buffer_lock(model.buffer) { + val snapshot = model.snapshot + + if (control) init_popup(snapshot, x, y) + highlight_range map { case (range, _) => invalidate_line_range(range) } - highlight_range = - if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None + highlight_range = if (control) subexp_range(snapshot, x, y) else None highlight_range map { case (range, _) => invalidate_line_range(range) } } } @@ -296,7 +309,7 @@ // gutter icons val icons = - (for (Text.Info(_, Some(icon)) <- + (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator) yield icon).toList.sortWith(_ >= _) icons match { @@ -400,6 +413,45 @@ } + /* main actor */ + + private val main_actor = actor { + loop { + react { + case Session.Commands_Changed(changed) => + val buffer = model.buffer + Isabelle.swing_buffer_lock(buffer) { + val snapshot = model.snapshot() + + if (changed.exists(snapshot.node.commands.contains)) + overview.repaint() + + val visible_range = screen_lines_range() + val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1) + if (visible_cmds.exists(changed)) { + for { + line <- 0 until text_area.getVisibleLines + val start = text_area.getScreenLineStartOffset(line) if start >= 0 + val end = text_area.getScreenLineEndOffset(line) if end >= 0 + val range = proper_line_range(start, end) + val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1) + if line_cmds.exists(changed) + } text_area.invalidateScreenLineRange(line, line) + + // FIXME danger of deadlock!? + // FIXME potentially slow!? + model.buffer.propertiesChanged() + } + } + + case Session.Global_Settings => html_panel_resize() + + case bad => System.err.println("command_change_actor: ignoring bad message " + bad) + } + } + } + + /* activation */ private def activate() @@ -411,17 +463,20 @@ text_area.getPainter.addMouseMotionListener(mouse_motion_listener) text_area.addCaretListener(caret_listener) text_area.addLeftOfScrollBar(overview) - session.commands_changed += commands_changed_actor + session.commands_changed += main_actor + session.global_settings += main_actor } private def deactivate() { - session.commands_changed -= commands_changed_actor + session.commands_changed -= main_actor + session.global_settings -= main_actor text_area.removeFocusListener(focus_listener) text_area.getPainter.removeMouseMotionListener(mouse_motion_listener) text_area.removeCaretListener(caret_listener) text_area.removeLeftOfScrollBar(overview) text_area.getGutter.removeExtension(gutter_extension) text_area.getPainter.removeExtension(text_area_extension) + exit_popup() } } \ No newline at end of file diff -r c7f0fa0593f0 -r 0294948ba962 src/Tools/jEdit/src/jedit/html_panel.scala --- a/src/Tools/jEdit/src/jedit/html_panel.scala Tue Sep 28 20:49:39 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Tue Sep 28 23:02:05 2010 +0200 @@ -118,6 +118,7 @@ private case class Resize(font_family: String, font_size: Int) private case class Render_Document(text: String) private case class Render(body: XML.Body) + private case class Render_Sync(body: XML.Body) private case object Refresh private val main_actor = actor { @@ -188,6 +189,7 @@ case Refresh => refresh() case Render_Document(text) => render_document(text) case Render(body) => render(body) + case Render_Sync(body) => render(body); reply(()) case bad => System.err.println("main_actor: ignoring bad message " + bad) } } @@ -200,4 +202,5 @@ def refresh() { main_actor ! Refresh } def render_document(text: String) { main_actor ! Render_Document(text) } def render(body: XML.Body) { main_actor ! Render(body) } + def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) } } diff -r c7f0fa0593f0 -r 0294948ba962 src/Tools/jEdit/src/jedit/isabelle_markup.scala --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Tue Sep 28 20:49:39 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Tue Sep 28 23:02:05 2010 +0200 @@ -84,6 +84,12 @@ case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color } + val popup: Markup_Tree.Select[XML.Tree] = + { + case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _)) + if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => msg + } + val gutter_message: Markup_Tree.Select[Icon] = { case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon