tuned GUI;
authorwenzelm
Sat, 15 Aug 2015 19:11:11 +0200
changeset 60936 2751f7f31be2
parent 60935 441c03582afa
child 60937 51425cbe8ce9
tuned GUI;
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))