--- 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)