# HG changeset patch
# User wenzelm
# Date 1729261895 -7200
# Node ID d9f087befd5c9ce7209d706661b2fe2b4fd61b61
# Parent  c66e24eae28175dedfa1d2c2042b47a1cd16b4dc
less instrusive rendering for input buffer (in contrast to 264f043c5da1);

diff -r c66e24eae281 -r d9f087befd5c src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Fri Oct 18 15:45:38 2024 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Fri Oct 18 16:31:35 2024 +0200
@@ -68,7 +68,7 @@
   val rich_text_area: Rich_Text_Area =
     new Rich_Text_Area(text_area.getView, text_area,
       () => Document_View.rendering(doc_view), () => (), () => None,
-      () => delay_caret_update.invoke(), caret_visible = true, enable_hovering = true)
+      () => delay_caret_update.invoke(), caret_visible = true, enable_hovering = false)
 
 
   /* perspective */