# HG changeset patch
# User wenzelm
# Date 1376044155 -7200
# Node ID 08bbd321ac4cec420f4b19d8d39d9e73d5344fbb
# Parent  eb7d7c0034b5e6f73a86419799fb270ba4472018
more active "provers" field, which increases chances that its history is stored;

diff -r eb7d7c0034b5 -r 08bbd321ac4c src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Aug 09 12:25:24 2013 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Aug 09 12:29:15 2013 +0200
@@ -101,6 +101,11 @@
   }
 
   private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
+    override def processKeyEvent(evt: KeyEvent)
+    {
+      if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
+      super.processKeyEvent(evt)
+    }
     setToolTipText(provers_label.tooltip)
     setColumns(20)
   }