--- a/src/Tools/jEdit/lib/Tools/jedit Tue Jun 14 08:33:51 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Jun 14 11:36:08 2011 +0200
@@ -23,7 +23,7 @@
"src/raw_output_dockable.scala"
"src/scala_console.scala"
"src/session_dockable.scala"
- "src/text_painter.scala"
+ "src/text_area_painter.scala"
)
declare -a RESOURCES=(
--- a/src/Tools/jEdit/src/document_view.scala Tue Jun 14 08:33:51 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Tue Jun 14 11:36:08 2011 +0200
@@ -162,7 +162,8 @@
}
}
- private var highlight_range: Option[(Text.Range, Color)] = None
+ @volatile private var _highlight_range: Option[(Text.Range, Color)] = None
+ def highlight_range(): Option[(Text.Range, Color)] = _highlight_range
/* CONTROL-mouse management */
@@ -172,12 +173,12 @@
private def exit_control()
{
exit_popup()
- highlight_range = None
+ _highlight_range = None
}
private val focus_listener = new FocusAdapter {
override def focusLost(e: FocusEvent) {
- highlight_range = None // FIXME exit_control !?
+ _highlight_range = None // FIXME exit_control !?
}
}
@@ -199,121 +200,20 @@
if (control) init_popup(snapshot, x, y)
- highlight_range map { case (range, _) => invalidate_line_range(range) }
- highlight_range = if (control) subexp_range(snapshot, x, y) else None
- highlight_range map { case (range, _) => invalidate_line_range(range) }
+ _highlight_range map { case (range, _) => invalidate_line_range(range) }
+ _highlight_range = if (control) subexp_range(snapshot, x, y) else None
+ _highlight_range map { case (range, _) => invalidate_line_range(range) }
}
}
}
- /* TextArea painting */
-
- @volatile private var _text_area_snapshot: Option[Document.Snapshot] = None
-
- def text_area_snapshot(): Document.Snapshot =
- _text_area_snapshot match {
- case Some(snapshot) => snapshot
- case None => error("Missing text area snapshot")
- }
-
- private val set_snapshot = new TextAreaExtension
- {
- override def paintScreenLineRange(gfx: Graphics2D,
- first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y: Int, line_height: Int)
- {
- _text_area_snapshot = Some(model.snapshot())
- }
- }
-
- private val reset_snapshot = new TextAreaExtension
- {
- override def paintScreenLineRange(gfx: Graphics2D,
- first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y: Int, line_height: Int)
- {
- _text_area_snapshot = None
- }
- }
-
- private val background_painter = new TextAreaExtension
- {
- override def paintScreenLineRange(gfx: Graphics2D,
- first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y: Int, line_height: Int)
- {
- Isabelle.swing_buffer_lock(model.buffer) {
- val snapshot = text_area_snapshot()
- val ascent = text_area.getPainter.getFontMetrics.getAscent
-
- for (i <- 0 until physical_lines.length) {
- if (physical_lines(i) != -1) {
- val line_range = proper_line_range(start(i), end(i))
+ /* text area painting */
- // background color: status
- val cmds = snapshot.node.command_range(snapshot.revert(line_range))
- for {
- (command, command_start) <- cmds if !command.is_ignored
- val range = line_range.restrict(snapshot.convert(command.range + command_start))
- r <- Isabelle.gfx_range(text_area, range)
- color <- Isabelle_Markup.status_color(snapshot, command)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
- }
-
- // background color (1): markup
- for {
- Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
- r <- Isabelle.gfx_range(text_area, range)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
- }
-
- // background color (2): markup
- for {
- Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
- r <- Isabelle.gfx_range(text_area, range)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
- }
+ private val text_area_painter = new Text_Area_Painter(this)
- // sub-expression highlighting -- potentially from other snapshot
- highlight_range match {
- case Some((range, color)) if line_range.overlaps(range) =>
- Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
- case None =>
- case Some(r) =>
- gfx.setColor(color)
- gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
- }
- case _ =>
- }
-
- // squiggly underline
- for {
- Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
- r <- Isabelle.gfx_range(text_area, range)
- } {
- gfx.setColor(color)
- val x0 = (r.x / 2) * 2
- val y0 = r.y + ascent + 1
- for (x1 <- Range(x0, x0 + r.length, 2)) {
- val y1 = if (x1 % 4 < 2) y0 else y0 + 1
- gfx.drawLine(x1, y1, x1 + 1, y1)
- }
- }
- }
- }
- }
- }
-
+ private val tooltip_painter = new TextAreaExtension
+ {
override def getToolTipText(x: Int, y: Int): String =
{
Isabelle.swing_buffer_lock(model.buffer) {
@@ -338,11 +238,6 @@
}
}
- val text_painter = new Text_Painter(this)
-
-
- /* Gutter painting */
-
private val gutter_painter = new TextAreaExtension
{
override def paintScreenLineRange(gfx: Graphics2D,
@@ -511,12 +406,8 @@
private def activate()
{
val painter = text_area.getPainter
-
- painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
- painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
- text_painter.activate()
- painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
-
+ painter.addExtension(TextAreaPainter.TEXT_LAYER, tooltip_painter)
+ text_area_painter.activate()
text_area.getGutter.addExtension(gutter_painter)
text_area.addFocusListener(focus_listener)
text_area.getView.addWindowListener(window_listener)
@@ -530,7 +421,6 @@
private def deactivate()
{
val painter = text_area.getPainter
-
session.commands_changed -= main_actor
session.global_settings -= main_actor
text_area.removeFocusListener(focus_listener)
@@ -539,11 +429,8 @@
text_area.removeCaretListener(caret_listener)
text_area.removeLeftOfScrollBar(overview)
text_area.getGutter.removeExtension(gutter_painter)
-
- painter.removeExtension(reset_snapshot)
- text_painter.deactivate()
- painter.removeExtension(background_painter)
- painter.removeExtension(set_snapshot)
+ text_area_painter.deactivate()
+ painter.removeExtension(tooltip_painter)
exit_popup()
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/text_area_painter.scala Tue Jun 14 11:36:08 2011 +0200
@@ -0,0 +1,286 @@
+/* Title: Tools/jEdit/src/text_area_painter.scala
+ Author: Makarius
+
+Painter setup for main jEdit text area.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.{Graphics, Graphics2D}
+import java.util.ArrayList
+
+import org.gjt.sp.jedit.Debug
+import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
+
+
+class Text_Area_Painter(doc_view: Document_View)
+{
+ private val model = doc_view.model
+ private val text_area = doc_view.text_area
+
+ private val orig_text_painter: TextAreaExtension =
+ {
+ val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
+ text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
+ match {
+ case List(x) => x
+ case _ => error("Expected exactly one " + name)
+ }
+ }
+
+
+ /* painter snapshot */
+
+ @volatile private var _painter_snapshot: Option[Document.Snapshot] = None
+
+ private def painter_snapshot(): Document.Snapshot =
+ _painter_snapshot match {
+ case Some(snapshot) => snapshot
+ case None => error("Missing document snapshot for text area painter")
+ }
+
+ private val set_snapshot = new TextAreaExtension
+ {
+ override def paintScreenLineRange(gfx: Graphics2D,
+ first_line: Int, last_line: Int, physical_lines: Array[Int],
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ {
+ _painter_snapshot = Some(model.snapshot())
+ }
+ }
+
+ private val reset_snapshot = new TextAreaExtension
+ {
+ override def paintScreenLineRange(gfx: Graphics2D,
+ first_line: Int, last_line: Int, physical_lines: Array[Int],
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ {
+ _painter_snapshot = None
+ }
+ }
+
+
+ /* text background */
+
+ private val background_painter = new TextAreaExtension
+ {
+ override def paintScreenLineRange(gfx: Graphics2D,
+ first_line: Int, last_line: Int, physical_lines: Array[Int],
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ {
+ Isabelle.swing_buffer_lock(model.buffer) {
+ val snapshot = painter_snapshot()
+ val ascent = text_area.getPainter.getFontMetrics.getAscent
+
+ for (i <- 0 until physical_lines.length) {
+ if (physical_lines(i) != -1) {
+ val line_range = doc_view.proper_line_range(start(i), end(i))
+
+ // background color: status
+ val cmds = snapshot.node.command_range(snapshot.revert(line_range))
+ for {
+ (command, command_start) <- cmds if !command.is_ignored
+ val range = line_range.restrict(snapshot.convert(command.range + command_start))
+ r <- Isabelle.gfx_range(text_area, range)
+ color <- Isabelle_Markup.status_color(snapshot, command)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+ }
+
+ // background color (1): markup
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+ }
+
+ // background color (2): markup
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
+ }
+
+ // sub-expression highlighting -- potentially from other snapshot
+ doc_view.highlight_range match {
+ case Some((range, color)) if line_range.overlaps(range) =>
+ Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
+ case None =>
+ case Some(r) =>
+ gfx.setColor(color)
+ gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
+ }
+ case _ =>
+ }
+
+ // squiggly underline
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ val x0 = (r.x / 2) * 2
+ val y0 = r.y + ascent + 1
+ for (x1 <- Range(x0, x0 + r.length, 2)) {
+ val y1 = if (x1 % 4 < 2) y0 else y0 + 1
+ gfx.drawLine(x1, y1, x1 + 1, y1)
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+
+ /* text */
+
+ private val text_painter = new TextAreaExtension
+ {
+ override def paintScreenLineRange(gfx: Graphics2D,
+ first_line: Int, last_line: Int, physical_lines: Array[Int],
+ start: Array[Int], end: Array[Int], y_start: Int, line_height: Int)
+ {
+ val buffer = text_area.getBuffer
+ Isabelle.swing_buffer_lock(buffer) {
+ val painter = text_area.getPainter
+ val font = painter.getFont
+ val font_context = painter.getFontRenderContext
+ val font_metrics = painter.getFontMetrics
+
+ def paint_chunk_list(head_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
+ {
+ val clip_rect = gfx.getClipBounds
+
+ var w = 0.0f
+ var offset = head_offset
+ var chunk = head
+ while (chunk != null) {
+ val chunk_length = if (chunk.str == null) 0 else chunk.str.length
+
+ if (x + w + chunk.width > clip_rect.x &&
+ x + w < clip_rect.x + clip_rect.width &&
+ chunk.accessable && chunk.visible)
+ {
+ val chunk_range = Text.Range(offset, offset + chunk_length)
+ val chunk_font = chunk.style.getFont
+ val chunk_color = chunk.style.getForegroundColor
+
+ val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
+
+ gfx.setFont(chunk_font)
+ if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
+ markup.forall(info => info.info.isEmpty)) {
+ gfx.setColor(chunk_color)
+ gfx.drawGlyphVector(chunk.gv, x + w, y)
+ }
+ else {
+ var xpos = x + w
+ for (Text.Info(range, info) <- markup) {
+ val str = chunk.str.substring(range.start - offset, range.stop - offset)
+ gfx.setColor(info.getOrElse(chunk_color))
+ gfx.drawString(str, xpos.toInt, y.toInt)
+ xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
+ }
+ }
+ }
+ w += chunk.width
+ offset += chunk_length
+ chunk = chunk.next.asInstanceOf[Chunk]
+ }
+ w
+ }
+
+ // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
+ // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
+ val char_width = font.getStringBounds(" ", font_context).getWidth.round.toInt
+ val soft_wrap = buffer.getStringProperty("wrap") == "soft"
+ val wrap_margin =
+ {
+ val max = buffer.getIntegerProperty("maxLineLen", 0)
+ if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
+ else if (soft_wrap) painter.getWidth - char_width * 3
+ else 0
+ }.toFloat
+
+ val line_infos: Map[Text.Offset, Chunk] =
+ {
+ val out = new ArrayList[Chunk]
+ val handler = new DisplayTokenHandler
+ val margin = if (soft_wrap) wrap_margin else 0.0f
+
+ var result = Map[Text.Offset, Chunk]()
+ for (line <- physical_lines.iterator.filter(i => i != -1)) {
+ out.clear
+ handler.init(painter.getStyles, font_context, painter, out, margin)
+ buffer.markTokens(line, handler)
+
+ val line_start = buffer.getLineStartOffset(line)
+ for (i <- 0 until out.size) {
+ val chunk = out.get(i)
+ result += (line_start + chunk.offset -> chunk)
+ }
+ }
+ result
+ }
+
+ val clip = gfx.getClip
+ val x0 = text_area.getHorizontalOffset
+ var y0 =
+ y_start + font_metrics.getHeight - (font_metrics.getLeading + 1) - font_metrics.getDescent
+
+ for (i <- 0 until physical_lines.length) {
+ if (physical_lines(i) != -1) {
+ line_infos.get(start(i)) match {
+ case Some(chunk) =>
+ val w = paint_chunk_list(start(i), chunk, x0, y0).toInt
+ gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
+ orig_text_painter.paintValidLine(gfx,
+ first_line + i, physical_lines(i), start(i), end(i), y_start + line_height * i)
+ gfx.setClip(clip)
+
+ case None =>
+ }
+ }
+ y0 += line_height
+ }
+ }
+ }
+ }
+
+
+ /* activation */
+
+ def activate()
+ {
+ val painter = text_area.getPainter
+ painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
+ painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
+ painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
+ painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
+ painter.removeExtension(orig_text_painter)
+ }
+
+ def deactivate()
+ {
+ val painter = text_area.getPainter
+ painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
+ painter.removeExtension(reset_snapshot)
+ painter.removeExtension(text_painter)
+ painter.removeExtension(background_painter)
+ painter.removeExtension(set_snapshot)
+ }
+}
+
--- a/src/Tools/jEdit/src/text_painter.scala Tue Jun 14 08:33:51 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,162 +0,0 @@
-/* Title: Tools/jEdit/src/text_painter.scala
- Author: Makarius
-
-Replacement painter for jEdit text area.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.awt.{Graphics, Graphics2D}
-import java.util.ArrayList
-
-import org.gjt.sp.jedit.Debug
-import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
-
-
-class Text_Painter(doc_view: Document_View) extends TextAreaExtension
-{
- private val text_area = doc_view.text_area
-
- private val orig_text_painter: TextAreaExtension =
- {
- val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
- text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
- match {
- case List(x) => x
- case _ => error("Expected exactly one " + name)
- }
- }
-
- override def paintScreenLineRange(gfx: Graphics2D,
- first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y_start: Int, line_height: Int)
- {
- val buffer = text_area.getBuffer
- Isabelle.swing_buffer_lock(buffer) {
- val painter = text_area.getPainter
- val font = painter.getFont
- val font_context = painter.getFontRenderContext
- val font_metrics = painter.getFontMetrics
-
- def paint_chunk_list(head_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
- {
- val clip_rect = gfx.getClipBounds
-
- var w = 0.0f
- var offset = head_offset
- var chunk = head
- while (chunk != null) {
- val chunk_length = if (chunk.str == null) 0 else chunk.str.length
-
- if (x + w + chunk.width > clip_rect.x &&
- x + w < clip_rect.x + clip_rect.width &&
- chunk.accessable && chunk.visible)
- {
- val chunk_range = Text.Range(offset, offset + chunk_length)
- val chunk_font = chunk.style.getFont
- val chunk_color = chunk.style.getForegroundColor
-
- val markup =
- doc_view.text_area_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
-
- gfx.setFont(chunk_font)
- if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
- markup.forall(info => info.info.isEmpty)) {
- gfx.setColor(chunk_color)
- gfx.drawGlyphVector(chunk.gv, x + w, y)
- }
- else {
- var xpos = x + w
- for (Text.Info(range, info) <- markup) {
- val str = chunk.str.substring(range.start - offset, range.stop - offset)
- gfx.setColor(info.getOrElse(chunk_color))
- gfx.drawString(str, xpos.toInt, y.toInt)
- xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
- }
- }
- }
- w += chunk.width
- offset += chunk_length
- chunk = chunk.next.asInstanceOf[Chunk]
- }
- w
- }
-
- // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
- // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
- val char_width = font.getStringBounds(" ", font_context).getWidth.round.toInt
- val soft_wrap = buffer.getStringProperty("wrap") == "soft"
- val wrap_margin =
- {
- val max = buffer.getIntegerProperty("maxLineLen", 0)
- if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
- else if (soft_wrap) painter.getWidth - char_width * 3
- else 0
- }.toFloat
-
- val line_infos: Map[Text.Offset, Chunk] =
- {
- val out = new ArrayList[Chunk]
- val handler = new DisplayTokenHandler
- val margin = if (soft_wrap) wrap_margin else 0.0f
-
- var result = Map[Text.Offset, Chunk]()
- for (line <- physical_lines.iterator.filter(i => i != -1)) {
- out.clear
- handler.init(painter.getStyles, font_context, painter, out, margin)
- buffer.markTokens(line, handler)
-
- val line_start = buffer.getLineStartOffset(line)
- for (i <- 0 until out.size) {
- val chunk = out.get(i)
- result += (line_start + chunk.offset -> chunk)
- }
- }
- result
- }
-
- val clip = gfx.getClip
- val x0 = text_area.getHorizontalOffset
- var y0 =
- y_start + font_metrics.getHeight - (font_metrics.getLeading + 1) - font_metrics.getDescent
-
- for (i <- 0 until physical_lines.length) {
- if (physical_lines(i) != -1) {
- line_infos.get(start(i)) match {
- case Some(chunk) =>
- val w = paint_chunk_list(start(i), chunk, x0, y0).toInt
- gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
- orig_text_painter.paintValidLine(gfx,
- first_line + i, physical_lines(i), start(i), end(i), y_start + line_height * i)
- gfx.setClip(clip)
-
- case None =>
- }
- }
- y0 += line_height
- }
- }
- }
-
-
- /* activation */
-
- def activate()
- {
- val painter = text_area.getPainter
- painter.removeExtension(orig_text_painter)
- painter.addExtension(TextAreaPainter.TEXT_LAYER, this)
- }
-
- def deactivate()
- {
- val painter = text_area.getPainter
- painter.removeExtension(this)
- painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
- }
-}
-