# HG changeset patch
# User wenzelm
# Date 1375865906 -7200
# Node ID 9e4bae21494da989ec7964175402bc164772d4aa
# Parent  45678f8e7a0f1fa47c412ef82e4b2b37ffcbf18b
prefer single-line HistoryTextField;

diff -r 45678f8e7a0f -r 9e4bae21494d src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Tue Aug 06 23:24:10 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Wed Aug 07 10:58:26 2013 +0200
@@ -18,7 +18,7 @@
 import java.awt.event.{ComponentEvent, ComponentAdapter}
 
 import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.gui.HistoryTextArea
+import org.gjt.sp.jedit.gui.HistoryTextField
 
 
 class Find_Dockable(view: View, position: String) extends Dockable(view, position)
@@ -91,10 +91,9 @@
 
   /* controls */
 
-  private val query = new HistoryTextArea("isabelle-find-theorems") {
+  private val query = new HistoryTextField("isabelle-find-theorems") {
     { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
-    setColumns(25)
-    setRows(1)
+    setColumns(40)
   }
 
   private val query_wrapped = Component.wrap(query)