# HG changeset patch
# User wenzelm
# Date 1399404557 -7200
# Node ID 38c6b70e5e53d8c7bb223806e1a4bdcae50bdfed
# Parent  6d4b2f8f010c4d95ee909c694126b40a641aa05f
common support for search field, which is actually a light-weight Highlighter;

diff -r 6d4b2f8f010c -r 38c6b70e5e53 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue May 06 17:47:03 2014 +0200
+++ b/src/Tools/jEdit/etc/options	Tue May 06 21:29:17 2014 +0200
@@ -105,6 +105,7 @@
 option operator_color : string = "323232FF"
 option caret_invisible_color : string = "50000080"
 option completion_color : string = "0000FFFF"
+option search_color : string = "66FFFF64"
 
 option tfree_color : string = "A020F0FF"
 option tvar_color : string = "A020F0FF"
diff -r 6d4b2f8f010c -r 38c6b70e5e53 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Tue May 06 17:47:03 2014 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Tue May 06 21:29:17 2014 +0200
@@ -64,7 +64,7 @@
 
   val rich_text_area =
     new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
-      caret_visible = true, enable_hovering = false)
+      () => None, caret_visible = true, enable_hovering = false)
 
 
   /* perspective */
diff -r 6d4b2f8f010c -r 38c6b70e5e53 src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Tue May 06 17:47:03 2014 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Tue May 06 21:29:17 2014 +0200
@@ -91,7 +91,8 @@
   private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
   zoom.tooltip = "Zoom factor for basic font size"
 
-  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(zoom)
+  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+    pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
   add(controls.peer, BorderLayout.NORTH)
 
 
diff -r 6d4b2f8f010c -r 38c6b70e5e53 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Tue May 06 17:47:03 2014 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Tue May 06 21:29:17 2014 +0200
@@ -140,9 +140,9 @@
     reactions += { case ButtonClicked(_) => handle_update(true, None) }
   }
 
-  private val detach = pretty_text_area.make_detach_button
-
   private val controls =
-    new Wrap_Panel(Wrap_Panel.Alignment.Right)(auto_update, update, detach, zoom)
+    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+      pretty_text_area.search_label, pretty_text_area.search_pattern,
+      auto_update, update, pretty_text_area.detach_button, zoom)
   add(controls.peer, BorderLayout.NORTH)
 }
diff -r 6d4b2f8f010c -r 38c6b70e5e53 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 06 17:47:03 2014 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Tue May 06 21:29:17 2014 +0200
@@ -12,10 +12,13 @@
 
 import java.awt.{Color, Font, FontMetrics, Toolkit, Window}
 import java.awt.event.KeyEvent
+import javax.swing.JTextField
+
 import java.util.concurrent.{Future => JFuture}
 
 import scala.swing.event.ButtonClicked
-import scala.swing.Button
+import scala.swing.{Button, Label, Component}
+import scala.util.matching.Regex
 
 import org.gjt.sp.jedit.{jEdit, View, Registers}
 import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
@@ -25,6 +28,8 @@
 
 object Pretty_Text_Area
 {
+  /* auxiliary */
+
   private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
     formatted_body: XML.Body): (String, Document.State) =
   {
@@ -75,7 +80,10 @@
 
   private val rich_text_area =
     new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
-      caret_visible = false, enable_hovering = true)
+      get_search_pattern _, caret_visible = false, enable_hovering = true)
+
+  private var current_search_pattern: Option[Regex] = None
+  def get_search_pattern(): Option[Regex] = Swing_Thread.require { current_search_pattern }
 
   def get_background(): Option[Color] = None
 
@@ -172,7 +180,47 @@
 
   /* common GUI components */
 
-  def make_detach_button: Button = new Button("Detach") {
+  val search_label: Component = new Label("Search:") {
+    tooltip = "Search and highlight output via regular expression"
+  }
+
+  val search_pattern: Component =
+    Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search")
+      {
+        private val input_delay =
+          Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
+            search_action(this)
+          }
+        override def processKeyEvent(evt: KeyEvent)
+        {
+          super.processKeyEvent(evt)
+          input_delay.invoke()
+        }
+        setColumns(20)
+        setToolTipText(search_label.tooltip)
+        setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
+      })
+
+  private val search_pattern_foreground = search_pattern.foreground
+
+  private def search_action(text_field: JTextField)
+  {
+    val (pattern, ok) =
+      text_field.getText match {
+        case null | "" => (None, true)
+        case s =>
+          try { (Some(new Regex(s)), true) }
+          catch { case ERROR(_) => (None, false) }
+      }
+    if (current_search_pattern != pattern) {
+      current_search_pattern = pattern
+      text_area.getPainter.repaint()
+    }
+    text_field.setForeground(
+      if (ok) search_pattern_foreground else current_rendering.error_color)
+  }
+
+  val detach_button: Component = new Button("Detach") {
     tooltip = "Detach window with static copy of current output"
     reactions += { case ButtonClicked(_) => text_area.detach }
   }
diff -r 6d4b2f8f010c -r 38c6b70e5e53 src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Tue May 06 17:47:03 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Tue May 06 21:29:17 2014 +0200
@@ -91,7 +91,7 @@
       query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
     }
 
-    private val query_label = new Label("Search criteria:") {
+    private val query_label = new Label("Query:") {
       tooltip =
         GUI.tooltip_lines(
           "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
@@ -120,12 +120,12 @@
       reactions += { case ButtonClicked(_) => apply_query() }
     }
 
-    private val detach = pretty_text_area.make_detach_button
-
     private val control_panel =
       new Wrap_Panel(Wrap_Panel.Alignment.Right)(
         query_label, Component.wrap(query), limit, allow_dups,
-        process_indicator.component, apply_button, detach)
+        process_indicator.component, apply_button,
+        pretty_text_area.search_label, pretty_text_area.search_pattern,
+        pretty_text_area.detach_button)
 
     def select { control_panel.contents += zoom }
 
@@ -156,7 +156,7 @@
       query_operation.apply_query(List(query.getText))
     }
 
-    private val query_label = new Label("Search criteria:") {
+    private val query_label = new Label("Query:") {
       tooltip = GUI.tooltip_lines("Name / type patterns for constants")
     }
 
@@ -170,11 +170,11 @@
       reactions += { case ButtonClicked(_) => apply_query() }
     }
 
-    private val detach = pretty_text_area.make_detach_button
-
     private val control_panel =
       new Wrap_Panel(Wrap_Panel.Alignment.Right)(
-        query_label, Component.wrap(query), process_indicator.component, apply_button, detach)
+        query_label, Component.wrap(query), process_indicator.component, apply_button,
+        pretty_text_area.search_label, pretty_text_area.search_pattern,
+        pretty_text_area.detach_button)
 
     def select { control_panel.contents += zoom }
 
@@ -252,15 +252,16 @@
       reactions += { case ButtonClicked(_) => apply_query() }
     }
 
-    private val detach = pretty_text_area.make_detach_button
-
     private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
 
     def select
     {
       set_selector()
       control_panel.contents.clear
-      control_panel.contents ++= List(query_label, selector, apply_button, detach, zoom)
+      control_panel.contents ++=
+        List(query_label, selector, apply_button,
+          pretty_text_area.search_label, pretty_text_area.search_pattern,
+          pretty_text_area.detach_button, zoom)
     }
 
     val page =
diff -r 6d4b2f8f010c -r 38c6b70e5e53 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Tue May 06 17:47:03 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Tue May 06 21:29:17 2014 +0200
@@ -246,6 +246,7 @@
   val operator_color = color_value("operator_color")
   val caret_invisible_color = color_value("caret_invisible_color")
   val completion_color = color_value("completion_color")
+  val search_color = color_value("search_color")
 
   val tfree_color = color_value("tfree_color")
   val tvar_color = color_value("tvar_color")
diff -r 6d4b2f8f010c -r 38c6b70e5e53 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Tue May 06 17:47:03 2014 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue May 06 21:29:17 2014 +0200
@@ -18,6 +18,8 @@
 import java.text.AttributedString
 import java.util.ArrayList
 
+import scala.util.matching.Regex
+
 import org.gjt.sp.util.Log
 import org.gjt.sp.jedit.{OperatingSystem, Debug, View}
 import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
@@ -29,6 +31,7 @@
   text_area: TextArea,
   get_rendering: () => Rendering,
   close_action: () => Unit,
+  get_search_pattern: () => Option[Regex],
   caret_visible: Boolean,
   enable_hovering: Boolean)
 {
@@ -495,6 +498,7 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       robust_rendering { rendering =>
+        val search_pattern = get_search_pattern()
         for (i <- 0 until physical_lines.length) {
           if (physical_lines(i) != -1) {
             val line_range = Text.Range(start(i), end(i))
@@ -508,6 +512,18 @@
               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
             }
 
+            // search pattern
+            for {
+              regex <- search_pattern
+              text <- JEdit_Lib.try_get_text(buffer, line_range)
+              m <- regex.findAllMatchIn(text)
+              range = Text.Range(m.start, m.end) + line_range.start
+              r <- JEdit_Lib.gfx_range(text_area, range)
+            } {
+              gfx.setColor(rendering.search_color)
+              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+            }
+
             // highlight range -- potentially from other snapshot
             for {
               info <- highlight_area.info