# HG changeset patch
# User wenzelm
# Date 1731683336 -3600
# Node ID b3a90bff348ae76b6a1854c8754730e0f6b1bf1f
# Parent  cc9fc6f375b24a0b745a747fa3c37e5dc3ae5af7
clarified key events: cancel output selection, before input selection;

diff -r cc9fc6f375b2 -r b3a90bff348a src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 15 16:04:26 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Nov 15 16:08:56 2024 +0100
@@ -251,6 +251,7 @@
 
         case KeyEvent.VK_ESCAPE =>
           if (Isabelle.dismissed_popups(view)) evt.consume()
+          else if (getSelectionCount != 0) { selectNone(); evt.consume() }
 
         case _ =>
       }