--- a/src/Pure/General/markup.scala Tue Jun 14 13:50:54 2011 +0200
+++ b/src/Pure/General/markup.scala Tue Jun 14 15:58:01 2011 +0200
@@ -167,6 +167,7 @@
val XNUM = "xnum"
val XSTR = "xstr"
val LITERAL = "literal"
+ val INNER_STRING = "inner_string"
val INNER_COMMENT = "inner_comment"
val TOKEN_RANGE = "token_range"
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Jun 14 13:50:54 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Jun 14 15:58:01 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=(
@@ -166,17 +166,27 @@
TARGET="dist/jars/Isabelle-jEdit.jar"
+declare -a UPDATED=()
+
if [ "$BUILD_JARS" = jars_fresh ]; then
OUTDATED=true
else
OUTDATED=false
if [ ! -e "$TARGET" ]; then
OUTDATED=true
- elif [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
- for SOURCE in "${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}"
+ else
+ if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
+ declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}")
+ else
+ declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}")
+ fi
+ for DEP in "${DEPS[@]}"
do
- [ ! -e "$SOURCE" ] && fail "Missing file: $SOURCE"
- [ "$SOURCE" -nt "$TARGET" ] && OUTDATED=true
+ [ ! -e "$DEP" ] && fail "Missing file: $DEP"
+ [ "$DEP" -nt "$TARGET" ] && {
+ OUTDATED=true
+ UPDATED["${#UPDATED[@]}"]="$DEP"
+ }
done
fi
fi
@@ -186,6 +196,14 @@
if [ "$OUTDATED" = true ]
then
+ [ "${#UPDATED[@]}" -gt 0 ] && {
+ echo "Rebuild due to updated file dependencies:"
+ for FILE in "${UPDATED[@]}"
+ do
+ echo " $FILE"
+ done
+ }
+
[ -z "$SCALA_HOME" ] && fail "Unknown SCALA_HOME -- Scala unavailable"
[ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
--- a/src/Tools/jEdit/src/document_view.scala Tue Jun 14 13:50:54 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Tue Jun 14 15:58:01 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.LINE_BACKGROUND_LAYER + 1, 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()
}
}
--- a/src/Tools/jEdit/src/isabelle_markup.scala Tue Jun 14 13:50:54 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Tue Jun 14 15:58:01 2011 +0200
@@ -11,6 +11,7 @@
import java.awt.Color
+import org.lobobrowser.util.gui.ColorFactory
import org.gjt.sp.jedit.syntax.Token
@@ -20,6 +21,8 @@
// see http://www.w3schools.com/css/css_colornames.asp
+ def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
+
val outdated_color = new Color(240, 240, 240)
val unfinished_color = new Color(255, 228, 225)
@@ -30,9 +33,8 @@
val bad_color = new Color(255, 106, 106, 100)
val hilite_color = new Color(255, 204, 102, 100)
- val free_color = new Color(0, 0, 0xFF)
- val skolem_color = new Color(0xD2, 0x69, 0x1E)
- val bound_color = new Color(0, 0x80, 0)
+ val keyword1_color = get_color("#006699")
+ val keyword2_color = get_color("#009966")
class Icon(val priority: Int, val icon: javax.swing.Icon)
{
@@ -106,11 +108,33 @@
case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
}
+ private val foreground_colors: Map[String, Color] =
+ Map(
+ Markup.TCLASS -> get_color("red"),
+ Markup.TFREE -> get_color("#A020F0"),
+ Markup.TVAR -> get_color("#A020F0"),
+ Markup.CONST -> get_color("dimgrey"),
+ Markup.FREE -> get_color("blue"),
+ Markup.SKOLEM -> get_color("#D2691E"),
+ Markup.BOUND -> get_color("green"),
+ Markup.VAR -> get_color("#00009B"),
+ Markup.INNER_STRING -> get_color("#D2691E"),
+ Markup.INNER_COMMENT -> get_color("#8B0000"),
+ Markup.DYNAMIC_FACT -> get_color("yellowgreen"),
+ Markup.LITERAL -> keyword1_color,
+ Markup.ML_KEYWORD -> keyword1_color,
+ Markup.ML_DELIMITER -> get_color("black"),
+ Markup.ML_NUMERAL -> get_color("red"),
+ Markup.ML_CHAR -> get_color("#D2691E"),
+ Markup.ML_STRING -> get_color("#D2691E"),
+ Markup.ML_COMMENT -> get_color("#8B0000"),
+ Markup.ML_MALFORMED -> get_color("#FF6A6A")
+ )
+
val foreground: Markup_Tree.Select[Color] =
{
- case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => free_color
- case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => skolem_color
- case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => bound_color
+ case Text.Info(_, XML.Elem(Markup(m, _), _))
+ if foreground_colors.isDefinedAt(m) => foreground_colors(m)
}
val tooltip: Markup_Tree.Select[String] =
@@ -162,39 +186,6 @@
{
import Token._
Map[String, Byte](
- // logical entities
- Markup.TCLASS -> NULL,
- Markup.TYCON -> NULL,
- Markup.FIXED -> NULL,
- Markup.CONST -> LITERAL2,
- Markup.DYNAMIC_FACT -> LABEL,
- // inner syntax
- Markup.TFREE -> NULL,
- Markup.FREE -> NULL,
- Markup.TVAR -> NULL,
- Markup.SKOLEM -> NULL,
- Markup.BOUND -> NULL,
- Markup.VAR -> NULL,
- Markup.NUM -> DIGIT,
- Markup.FLOAT -> DIGIT,
- Markup.XNUM -> DIGIT,
- Markup.XSTR -> LITERAL4,
- Markup.LITERAL -> OPERATOR,
- Markup.INNER_COMMENT -> COMMENT1,
- Markup.SORT -> NULL,
- Markup.TYP -> NULL,
- Markup.TERM -> NULL,
- Markup.PROP -> NULL,
- // ML syntax
- Markup.ML_KEYWORD -> KEYWORD1,
- Markup.ML_DELIMITER -> OPERATOR,
- Markup.ML_IDENT -> NULL,
- Markup.ML_TVAR -> NULL,
- Markup.ML_NUMERAL -> DIGIT,
- Markup.ML_CHAR -> LITERAL1,
- Markup.ML_STRING -> LITERAL1,
- Markup.ML_COMMENT -> COMMENT1,
- Markup.ML_MALFORMED -> INVALID,
// embedded source text
Markup.ML_SOURCE -> COMMENT3,
Markup.DOC_SOURCE -> COMMENT3,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/text_area_painter.scala Tue Jun 14 15:58:01 2011 +0200
@@ -0,0 +1,284 @@
+/* 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.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.{TextAreaExtension, TextAreaPainter}
+
+
+class Text_Area_Painter(doc_view: Document_View)
+{
+ private val model = doc_view.model
+ private val buffer = model.buffer
+ 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(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 def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
+ {
+ val painter = text_area.getPainter
+ val font = painter.getFont
+ val font_context = painter.getFontRenderContext
+
+ // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
+ // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
+ val margin =
+ if (buffer.getStringProperty("wrap") != "soft") 0.0f
+ else {
+ val max = buffer.getIntegerProperty("maxLineLen", 0)
+ if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
+ else painter.getWidth - font.getStringBounds(" ", font_context).getWidth.round.toInt * 3
+ }.toFloat
+
+ val out = new ArrayList[Chunk]
+ val handler = new DisplayTokenHandler
+
+ var result = Map[Text.Offset, Chunk]()
+ for (line <- physical_lines) {
+ 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
+ }
+
+ private def paint_chunk_list(gfx: Graphics2D,
+ offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
+ {
+ val clip_rect = gfx.getClipBounds
+ val font_context = text_area.getPainter.getFontRenderContext
+
+ var w = 0.0f
+ var chunk_offset = 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(chunk_offset, chunk_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 x1 = x + w
+ for (Text.Info(range, info) <- markup) {
+ val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
+ gfx.setColor(info.getOrElse(chunk_color))
+ gfx.drawString(str, x1.toInt, y.toInt)
+ x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
+ }
+ }
+ }
+ w += chunk.width
+ chunk_offset += chunk_length
+ chunk = chunk.next.asInstanceOf[Chunk]
+ }
+ w
+ }
+
+ 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: Int, line_height: Int)
+ {
+ Isabelle.swing_buffer_lock(buffer) {
+ val clip = gfx.getClip
+ val x0 = text_area.getHorizontalOffset
+ val fm = text_area.getPainter.getFontMetrics
+ var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
+
+ val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
+ for (i <- 0 until physical_lines.length) {
+ if (physical_lines(i) != -1) {
+ infos.get(start(i)) match {
+ case Some(chunk) =>
+ val w = paint_chunk_list(gfx, 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 + 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 13:50:54 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)
- }
-}
-