disable broken popups for now;
authorwenzelm
Tue, 26 Oct 2010 16:56:07 +0200
changeset 40154 e11da4ec9d74
parent 40153 b6fe3b189725
child 40155 0b57e3d9bc62
disable broken popups for now;
src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Oct 26 15:57:16 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Oct 26 16:56:07 2010 +0200
@@ -130,6 +130,7 @@
   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)
 
@@ -143,6 +144,7 @@
         html_popup = Some(popup)
       case _ =>
     }
+*/
   }