tooltip: HTML dummy;
authorwenzelm
Tue, 15 Sep 2009 20:39:00 +0200
changeset 34735 2997f2a0f831
parent 34734 02479f4ac9a5
child 34736 ff7734c8bdb7
tooltip: HTML dummy;
src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Tue Sep 15 20:30:17 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Tue Sep 15 20:39:00 2009 +0200
@@ -52,7 +52,7 @@
     val buffer = text_area.getBuffer
     val lineCount = buffer.getLineCount
     val line = y_to_line(event.getY())
-    if (line >= 0 && line < text_area.getLineCount) "TODO: Tooltip"
+    if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
     else ""
   }