# HG changeset patch # User wenzelm # Date 1349368111 -7200 # Node ID 2d1cbdf6a68bd0007d0f6447df1d8cbb844b0d75 # Parent 1301ed1157298c91d70d823aa822c28821ad36ef Rich_Text_Area tooltips via nested Pretty_Text_Area, based on some techniques of FoldViewer plugin; diff -r 1301ed115729 -r 2d1cbdf6a68b src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Thu Oct 04 13:56:32 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Thu Oct 04 18:28:31 2012 +0200 @@ -259,13 +259,10 @@ } - private def tooltip_text(msg: XML.Tree): String = - Pretty.string_of(List(msg), margin = options.int("jedit_tooltip_margin")) - - def tooltip_message(range: Text.Range): Option[String] = + def tooltip_message(range: Text.Range): XML.Body = { val msgs = - snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty, + snapshot.cumulate_markup[SortedMap[Long, XML.Tree]](range, SortedMap.empty, Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR, Isabelle_Markup.BAD)), { @@ -274,11 +271,11 @@ if markup == Isabelle_Markup.WRITELN || markup == Isabelle_Markup.WARNING || markup == Isabelle_Markup.ERROR => - msgs + (serial -> tooltip_text(msg)) + msgs + (serial -> msg) case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), body))) - if !body.isEmpty => msgs + (Document.new_id() -> tooltip_text(msg)) + if !body.isEmpty => msgs + (Document.new_id() -> msg) }).toList.flatMap(_.info) - if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2))) + Library.separate(Pretty.Separator, msgs.iterator.map(_._2).toList) } @@ -302,38 +299,37 @@ Set(Isabelle_Markup.ENTITY, Isabelle_Markup.SORTING, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING, Isabelle_Markup.PATH) ++ tooltips.keys - private def string_of_typing(kind: String, body: XML.Body): String = - Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)), - margin = options.int("jedit_tooltip_margin")) + private def pretty_typing(kind: String, body: XML.Body): XML.Tree = + Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body) - def tooltip(range: Text.Range): Option[String] = + def tooltip(range: Text.Range): XML.Body = { - def add(prev: Text.Info[List[(Boolean, String)]], r: Text.Range, p: (Boolean, String)) = + def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r: Text.Range, p: (Boolean, XML.Tree)) = if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p)) val tips = - snapshot.cumulate_markup[Text.Info[(List[(Boolean, String)])]]( + snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]]( range, Text.Info(range, Nil), Some(tooltip_elements), { case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) => val kind1 = space_explode('_', kind).mkString(" ") - add(prev, r, (true, kind1 + " " + quote(name))) + add(prev, r, (true, XML.Text(kind1 + " " + quote(name)))) case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _))) if Path.is_ok(name) => val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name)) - add(prev, r, (true, "file " + quote(jedit_file))) + add(prev, r, (true, XML.Text("file " + quote(jedit_file)))) case (prev, Text.Info(r, XML.Elem(Markup(name, _), body))) if name == Isabelle_Markup.SORTING || name == Isabelle_Markup.TYPING => - add(prev, r, (true, string_of_typing("::", body))) + add(prev, r, (true, pretty_typing("::", body))) case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) => - add(prev, r, (false, string_of_typing("ML:", body))) + add(prev, r, (false, pretty_typing("ML:", body))) case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) - if tooltips.isDefinedAt(name) => add(prev, r, (true, tooltips(name))) + if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name)))) }).toList.flatMap(_.info.info) val all_tips = (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2) - if (all_tips.isEmpty) None else Some(cat_lines(all_tips)) + Library.separate(Pretty.FBreak, all_tips.toList) } diff -r 1301ed115729 -r 2d1cbdf6a68b src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Oct 04 13:56:32 2012 +0200 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Oct 04 18:28:31 2012 +0200 @@ -40,8 +40,6 @@ val version0 = base_snapshot.version val nodes0 = version0.nodes - assert(nodes0(node_name).commands.isEmpty) - val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) val version1 = Document.Version.make(version0.syntax, nodes1) val state1 = diff -r 1301ed115729 -r 2d1cbdf6a68b src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Thu Oct 04 13:56:32 2012 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Oct 04 18:28:31 2012 +0200 @@ -10,12 +10,14 @@ import isabelle._ -import java.awt.{Graphics2D, Shape, Window, Color} +import java.awt.{Graphics2D, Shape, Window, Color, Point, BorderLayout} import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent, FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} import java.awt.font.TextAttribute import java.text.AttributedString import java.util.ArrayList +import javax.swing.{SwingUtilities, JWindow, JPanel} +import javax.swing.border.LineBorder import org.gjt.sp.util.Log import org.gjt.sp.jedit.{OperatingSystem, Debug, View} @@ -198,12 +200,43 @@ { robust_body(null: String) { val rendering = get_rendering() - val offset = text_area.xyToOffset(x, y) - val range = Text.Range(offset, offset + 1) - val tip = - if (control) rendering.tooltip(range) - else rendering.tooltip_message(range) - tip.map(Isabelle.tooltip(_)) getOrElse null + val snapshot = rendering.snapshot + if (!snapshot.is_outdated) { + val offset = text_area.xyToOffset(x, y) + val range = Text.Range(offset, offset + 1) + val tip = + if (control) rendering.tooltip(range) + else rendering.tooltip_message(range) + if (!tip.isEmpty) { + val point = { + val painter = text_area.getPainter + val bounds = painter.getBounds() + val point = new Point(bounds.x + x, bounds.y + painter.getFontMetrics.getHeight + y) + SwingUtilities.convertPointToScreen(point, painter) + point + } + + val tooltip_text = new Pretty_Text_Area(view) + tooltip_text.resize(Isabelle.font_family(), Isabelle.font_size().round) // FIXME tooltip_scale + tooltip_text.update(snapshot, tip) + + val window = new JWindow(view) { + addWindowFocusListener(new WindowAdapter { + override def windowLostFocus(e: WindowEvent) { dispose() } + }) + setContentPane(new JPanel(new BorderLayout) { + override def getFocusTraversalKeysEnabled(): Boolean = false + }) + getRootPane.setBorder(new LineBorder(Color.BLACK)) + + add(tooltip_text) + setSize(300, 100) + setLocation(point.x, point.y) + setVisible(true) + } + } + } + null } } }