--- a/src/Tools/jEdit/src/completion_popup.scala Tue Sep 24 18:42:44 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Tue Sep 24 19:41:14 2013 +0200
@@ -13,6 +13,7 @@
import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
import javax.swing.border.LineBorder
+import javax.swing.text.DefaultCaret
import scala.swing.{ListView, ScrollPane}
import scala.swing.event.MouseClicked
@@ -221,6 +222,8 @@
{
text_field =>
+ // see https://forums.oracle.com/thread/1361677
+ if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret)
private var completion_popup: Option[Completion_Popup] = None