prefer single-line HistoryTextField;
authorwenzelm
Wed, 07 Aug 2013 10:58:26 +0200
changeset 52885 9e4bae21494d
parent 52882 45678f8e7a0f
child 52886 1e22e8101f47
prefer single-line HistoryTextField;
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)