--- 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"
--- 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 */
--- 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)
--- 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)
}
--- 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 }
}
--- 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 =
--- 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")
--- 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