# HG changeset patch
# User wenzelm
# Date 1439658671 -7200
# Node ID 2751f7f31be2666180270b78157978b2dc2532cb
# Parent  441c03582afa022a5547577c1dcf7c5759b2b134
tuned GUI;

diff -r 441c03582afa -r 2751f7f31be2 src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Sat Aug 15 19:07:11 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Sat Aug 15 19:11:11 2015 +0200
@@ -262,6 +262,12 @@
   private val context_field =
     new Completion_Popup.History_Text_Field("isabelle-debugger-context")
     {
+      override def processKeyEvent(evt: KeyEvent)
+      {
+        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
+          eval_expression()
+        super.processKeyEvent(evt)
+      }
       setColumns(20)
       setToolTipText(context_label.tooltip)
       setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))