# HG changeset patch
# User wenzelm
# Date 1400676165 -7200
# Node ID 5576d22abf3cb998f442d70f7a12e6194904fe3f
# Parent  fc96f394c7e58a3ce551f09f29b0d601df84b762
tuned signature;

diff -r fc96f394c7e5 -r 5576d22abf3c src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Wed May 21 14:09:43 2014 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Wed May 21 14:42:45 2014 +0200
@@ -92,7 +92,7 @@
   zoom.tooltip = "Zoom factor for basic font size"
 
   private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-    pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
+    pretty_text_area.search_label, pretty_text_area.search_field, zoom)
   add(controls.peer, BorderLayout.NORTH)
 
 
diff -r fc96f394c7e5 -r 5576d22abf3c src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Wed May 21 14:09:43 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed May 21 14:42:45 2014 +0200
@@ -144,6 +144,6 @@
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update,
-      pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
+      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }
diff -r fc96f394c7e5 -r 5576d22abf3c src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed May 21 14:09:43 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed May 21 14:42:45 2014 +0200
@@ -187,7 +187,7 @@
     tooltip = "Search and highlight output via regular expression"
   }
 
-  val search_pattern: Component =
+  val search_field: Component =
     Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search")
       {
         private val input_delay =
@@ -204,7 +204,7 @@
         setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
       })
 
-  private val search_pattern_foreground = search_pattern.foreground
+  private val search_field_foreground = search_field.foreground
 
   private def search_action(text_field: JTextField)
   {
@@ -220,7 +220,7 @@
       text_area.getPainter.repaint()
     }
     text_field.setForeground(
-      if (ok) search_pattern_foreground else current_rendering.error_color)
+      if (ok) search_field_foreground else current_rendering.error_color)
   }
 
 
diff -r fc96f394c7e5 -r 5576d22abf3c src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Wed May 21 14:09:43 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Wed May 21 14:42:45 2014 +0200
@@ -125,7 +125,7 @@
       new Wrap_Panel(Wrap_Panel.Alignment.Right)(
         query_label, Component.wrap(query), limit, allow_dups,
         process_indicator.component, apply_button,
-        pretty_text_area.search_label, pretty_text_area.search_pattern)
+        pretty_text_area.search_label, pretty_text_area.search_field)
 
     def select { control_panel.contents += zoom }
 
@@ -173,7 +173,7 @@
     private val control_panel =
       new Wrap_Panel(Wrap_Panel.Alignment.Right)(
         query_label, Component.wrap(query), process_indicator.component, apply_button,
-        pretty_text_area.search_label, pretty_text_area.search_pattern)
+        pretty_text_area.search_label, pretty_text_area.search_field)
 
     def select { control_panel.contents += zoom }
 
@@ -268,7 +268,7 @@
       control_panel.contents.clear
       control_panel.contents ++=
         List(query_label, selector, process_indicator.component, apply_button,
-          pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
+          pretty_text_area.search_label, pretty_text_area.search_field, zoom)
     }
 
     val page =
diff -r fc96f394c7e5 -r 5576d22abf3c src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 14:09:43 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 14:42:45 2014 +0200
@@ -191,7 +191,7 @@
 
   private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
     pretty_text_area.search_label,
-    pretty_text_area.search_pattern)
+    pretty_text_area.search_field)
 
   peer.add(controls.peer, BorderLayout.NORTH)
 }