# HG changeset patch
# User wenzelm
# Date 1288104967 -7200
# Node ID e11da4ec9d7451ae6dc6a3f3b061e2940428975d
# Parent  b6fe3b18972546c6e747f32c896c22111876e7bf
disable broken popups for now;

diff -r b6fe3b189725 -r e11da4ec9d74 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 _ =>
     }
+*/
   }