src/Tools/jEdit/src/pretty_text_area.scala

   private var current_base_snapshot = Document.State.init.snapshot()
   private var current_rendering: Rendering =
     Pretty_Text_Area.text_rendering(current_base_snapshot, Nil)._2
   private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
 
-  private val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering, true)
+  private val rich_text_area =
+    new Rich_Text_Area(view, text_area, () => current_rendering,
+      caret_visible = false, hovering = true)
 
   def refresh()
   {
     Swing_Thread.require()
 

       Toolkit.getDefaultToolkit().getMenuShortcutKeyMask()), JComponent.WHEN_FOCUSED)
 
 
   /* init */
 
-  override def isCaretVisible: Boolean = false
-
   getPainter.setStructureHighlightEnabled(false)
   getPainter.setLineHighlightEnabled(false)
 
   getBuffer.setTokenMarker(new Token_Markup.Marker(true, None))
   getBuffer.setReadOnly(true)