tuned signature;
authorwenzelm
Wed May 21 14:42:45 2014 +0200 (2014-05-21)
changeset 570425576d22abf3c
parent 57040 fc96f394c7e5
child 57043 0f44d6dbd2a4
tuned signature;
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/query_dockable.scala
src/Tools/jEdit/src/simplifier_trace_window.scala
     1.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Wed May 21 14:09:43 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Wed May 21 14:42:45 2014 +0200
     1.3 @@ -92,7 +92,7 @@
     1.4    zoom.tooltip = "Zoom factor for basic font size"
     1.5  
     1.6    private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
     1.7 -    pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
     1.8 +    pretty_text_area.search_label, pretty_text_area.search_field, zoom)
     1.9    add(controls.peer, BorderLayout.NORTH)
    1.10  
    1.11  
     2.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Wed May 21 14:09:43 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Wed May 21 14:42:45 2014 +0200
     2.3 @@ -144,6 +144,6 @@
     2.4  
     2.5    private val controls =
     2.6      new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update,
     2.7 -      pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
     2.8 +      pretty_text_area.search_label, pretty_text_area.search_field, zoom)
     2.9    add(controls.peer, BorderLayout.NORTH)
    2.10  }
     3.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed May 21 14:09:43 2014 +0200
     3.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed May 21 14:42:45 2014 +0200
     3.3 @@ -187,7 +187,7 @@
     3.4      tooltip = "Search and highlight output via regular expression"
     3.5    }
     3.6  
     3.7 -  val search_pattern: Component =
     3.8 +  val search_field: Component =
     3.9      Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search")
    3.10        {
    3.11          private val input_delay =
    3.12 @@ -204,7 +204,7 @@
    3.13          setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
    3.14        })
    3.15  
    3.16 -  private val search_pattern_foreground = search_pattern.foreground
    3.17 +  private val search_field_foreground = search_field.foreground
    3.18  
    3.19    private def search_action(text_field: JTextField)
    3.20    {
    3.21 @@ -220,7 +220,7 @@
    3.22        text_area.getPainter.repaint()
    3.23      }
    3.24      text_field.setForeground(
    3.25 -      if (ok) search_pattern_foreground else current_rendering.error_color)
    3.26 +      if (ok) search_field_foreground else current_rendering.error_color)
    3.27    }
    3.28  
    3.29  
     4.1 --- a/src/Tools/jEdit/src/query_dockable.scala	Wed May 21 14:09:43 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/query_dockable.scala	Wed May 21 14:42:45 2014 +0200
     4.3 @@ -125,7 +125,7 @@
     4.4        new Wrap_Panel(Wrap_Panel.Alignment.Right)(
     4.5          query_label, Component.wrap(query), limit, allow_dups,
     4.6          process_indicator.component, apply_button,
     4.7 -        pretty_text_area.search_label, pretty_text_area.search_pattern)
     4.8 +        pretty_text_area.search_label, pretty_text_area.search_field)
     4.9  
    4.10      def select { control_panel.contents += zoom }
    4.11  
    4.12 @@ -173,7 +173,7 @@
    4.13      private val control_panel =
    4.14        new Wrap_Panel(Wrap_Panel.Alignment.Right)(
    4.15          query_label, Component.wrap(query), process_indicator.component, apply_button,
    4.16 -        pretty_text_area.search_label, pretty_text_area.search_pattern)
    4.17 +        pretty_text_area.search_label, pretty_text_area.search_field)
    4.18  
    4.19      def select { control_panel.contents += zoom }
    4.20  
    4.21 @@ -268,7 +268,7 @@
    4.22        control_panel.contents.clear
    4.23        control_panel.contents ++=
    4.24          List(query_label, selector, process_indicator.component, apply_button,
    4.25 -          pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
    4.26 +          pretty_text_area.search_label, pretty_text_area.search_field, zoom)
    4.27      }
    4.28  
    4.29      val page =
     5.1 --- a/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 14:09:43 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Wed May 21 14:42:45 2014 +0200
     5.3 @@ -191,7 +191,7 @@
     5.4  
     5.5    private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
     5.6      pretty_text_area.search_label,
     5.7 -    pretty_text_area.search_pattern)
     5.8 +    pretty_text_area.search_field)
     5.9  
    5.10    peer.add(controls.peer, BorderLayout.NORTH)
    5.11  }