less tiny font for search criteria;

--- a/src/Pure/GUI/gui.scala	Wed Nov 06 18:04:36 2013 +0100
+++ b/src/Pure/GUI/gui.scala	Wed Nov 06 18:15:25 2013 +0100
@@ -168,10 +168,11 @@
   def font_metrics(font: Font): LineMetrics =
     font.getLineMetrics("", new FontRenderContext(null, false, false))
 
-  def imitate_font(family: String, font: Font): Font =
+  def imitate_font(family: String, font: Font, scale: Double = 1.0): Font =
   {
     val font1 = new Font(family, font.getStyle, font.getSize)
-    font1.deriveFont(font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
+    val size = scale * (font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
+    font1.deriveFont(size.round.toInt)
   }
 
   def transform_font(font: Font, transform: AffineTransform): Font =

--- a/src/Tools/jEdit/src/find_dockable.scala	Wed Nov 06 18:04:36 2013 +0100
+++ b/src/Tools/jEdit/src/find_dockable.scala	Wed Nov 06 18:15:25 2013 +0100
@@ -121,7 +121,7 @@
     { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
     setColumns(40)
     setToolTipText(query_label.tooltip)
-    setFont(GUI.imitate_font(Rendering.font_family(), getFont))
+    setFont(GUI.imitate_font(Rendering.font_family(), getFont, 1.2))
   }
 
   private case class Context_Entry(val name: String, val description: String)