--- a/src/Tools/jEdit/src/document_view.scala Mon Sep 17 18:14:54 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Mon Sep 17 20:23:25 2012 +0200
@@ -17,13 +17,9 @@
import java.lang.System
import java.text.BreakIterator
import java.awt.{Color, Graphics2D, Point}
-import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
- FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
import javax.swing.event.{CaretListener, CaretEvent}
-import org.gjt.sp.util.Log
-
-import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
+import org.gjt.sp.jedit.{jEdit, Debug}
import org.gjt.sp.jedit.gui.RolloverButton
import org.gjt.sp.jedit.options.GutterOptionPane
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
@@ -72,22 +68,6 @@
private val session = model.session
- /* robust extension body */
-
- def robust_body[A](default: A)(body: => A): A =
- {
- try {
- Swing_Thread.require()
- if (model.buffer == text_area.getBuffer) body
- else {
- Log.log(Log.ERROR, this, ERROR("Inconsistent document model"))
- default
- }
- }
- catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
- }
-
-
/* perspective */
def perspective(): Text.Perspective =
@@ -117,97 +97,12 @@
}
- /* active areas within the text */
-
- private class Active_Area[A](
- rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
- {
- private var the_info: Option[Text.Info[A]] = None
-
- def info: Option[Text.Info[A]] = the_info
-
- def update(new_info: Option[Text.Info[A]])
- {
- val old_info = the_info
- if (new_info != old_info) {
- for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
- JEdit_Lib.invalidate_range(text_area, range)
- the_info = new_info
- }
- }
-
- def update_rendering(r: Isabelle_Rendering, range: Text.Range)
- { update(rendering(r)(range)) }
-
- def reset { update(None) }
- }
-
- // owned by Swing thread
-
- private var control: Boolean = false
-
- private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
- def highlight_info(): Option[Text.Info[Color]] = highlight_area.info
-
- private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
- def hyperlink_info(): Option[Text.Info[Hyperlink]] = hyperlink_area.info
-
- private val active_areas = List(highlight_area, hyperlink_area)
- private def active_reset(): Unit = active_areas.foreach(_.reset)
-
- private val focus_listener = new FocusAdapter {
- override def focusLost(e: FocusEvent) { active_reset() }
- }
-
- private val window_listener = new WindowAdapter {
- override def windowIconified(e: WindowEvent) { active_reset() }
- override def windowDeactivated(e: WindowEvent) { active_reset() }
- }
-
- private val mouse_listener = new MouseAdapter {
- override def mouseClicked(e: MouseEvent) {
- hyperlink_area.info match {
- case Some(Text.Info(range, link)) => link.follow(text_area.getView)
- case None =>
- }
- }
- }
-
- private val mouse_motion_listener = new MouseMotionAdapter {
- override def mouseMoved(e: MouseEvent) {
- control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
- if (control && model.buffer.isLoaded) {
- JEdit_Lib.buffer_lock(model.buffer) {
- val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
- val mouse_range =
- JEdit_Lib.point_range(model.buffer, text_area.xyToOffset(e.getX(), e.getY()))
- active_areas.foreach(_.update_rendering(rendering, mouse_range))
- }
- }
- else active_reset()
- }
- }
-
-
/* text area painting */
- private val text_area_painter = new Text_Area_Painter(this)
+ def get_rendering(): Isabelle_Rendering =
+ Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
- private val tooltip_painter = new TextAreaExtension
- {
- override def getToolTipText(x: Int, y: Int): String =
- {
- robust_body(null: String) {
- val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
- val offset = text_area.xyToOffset(x, y)
- val range = Text.Range(offset, offset + 1)
- val tip =
- if (control) rendering.tooltip(range)
- else rendering.tooltip_message(range)
- tip.map(Isabelle.tooltip(_)) getOrElse null
- }
- }
- }
+ val text_area_painter = new Text_Area_Painter(text_area.getView, text_area, get_rendering _)
private val gutter_painter = new TextAreaExtension
{
@@ -215,7 +110,7 @@
first_line: Int, last_line: Int, physical_lines: Array[Int],
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
- robust_body(()) {
+ text_area_painter.robust_body(()) {
Swing_Thread.assert()
val gutter = text_area.getGutter
@@ -226,7 +121,7 @@
if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
val buffer = model.buffer
JEdit_Lib.buffer_lock(buffer) {
- val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
+ val rendering = get_rendering()
for (i <- 0 until physical_lines.length) {
if (physical_lines(i) != -1) {
@@ -328,14 +223,10 @@
private def activate()
{
val painter = text_area.getPainter
+
painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
- 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)
- painter.addMouseListener(mouse_listener)
- painter.addMouseMotionListener(mouse_motion_listener)
text_area.addCaretListener(caret_listener)
text_area.addLeftOfScrollBar(overview)
session.raw_edits += main_actor
@@ -345,17 +236,13 @@
private def deactivate()
{
val painter = text_area.getPainter
+
session.raw_edits -= main_actor
session.commands_changed -= main_actor
- text_area.removeFocusListener(focus_listener)
- text_area.getView.removeWindowListener(window_listener)
- painter.removeMouseMotionListener(mouse_motion_listener)
- painter.removeMouseListener(mouse_listener)
text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
text_area.getGutter.removeExtension(gutter_painter)
text_area_painter.deactivate()
- painter.removeExtension(tooltip_painter)
painter.removeExtension(update_perspective)
}
}
--- a/src/Tools/jEdit/src/output_dockable.scala Mon Sep 17 18:14:54 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Mon Sep 17 20:23:25 2012 +0200
@@ -47,7 +47,7 @@
val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get
Document_View(view.getTextArea) match {
case Some(doc_view) =>
- doc_view.robust_body() {
+ doc_view.text_area_painter.robust_body() {
val cmd = current_state.command
val model = doc_view.model
val buffer = model.buffer
--- a/src/Tools/jEdit/src/text_area_painter.scala Mon Sep 17 18:14:54 2012 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala Mon Sep 17 20:23:25 2012 +0200
@@ -9,21 +9,38 @@
import isabelle._
-import java.awt.{Graphics2D, Shape}
+import java.awt.{Graphics2D, Shape, Window, Color}
+import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
+ FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
import java.awt.font.TextAttribute
import java.text.AttributedString
import java.util.ArrayList
-import org.gjt.sp.jedit.Debug
+import org.gjt.sp.util.Log
+import org.gjt.sp.jedit.{OperatingSystem, Debug, View}
import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
-import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
+
+
+class Text_Area_Painter(view: View, text_area: TextArea, get_rendering: () => Isabelle_Rendering)
+{
+ private val buffer = text_area.getBuffer
-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
+ /* robust extension body */
+
+ def robust_body[A](default: A)(body: => A): A =
+ {
+ try {
+ Swing_Thread.require()
+ if (buffer == text_area.getBuffer) body
+ else {
+ Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
+ default
+ }
+ }
+ catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
+ }
/* original painters */
@@ -52,7 +69,7 @@
first_line: Int, last_line: Int, physical_lines: Array[Int],
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
- painter_rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
+ painter_rendering = get_rendering()
painter_clip = gfx.getClip
}
}
@@ -70,7 +87,94 @@
private def robust_rendering(body: Isabelle_Rendering => Unit)
{
- doc_view.robust_body(()) { body(painter_rendering) }
+ robust_body(()) { body(painter_rendering) }
+ }
+
+
+ /* active areas within the text */
+
+ private class Active_Area[A](
+ rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
+ {
+ private var the_info: Option[Text.Info[A]] = None
+
+ def info: Option[Text.Info[A]] = the_info
+
+ def update(new_info: Option[Text.Info[A]])
+ {
+ val old_info = the_info
+ if (new_info != old_info) {
+ for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
+ JEdit_Lib.invalidate_range(text_area, range)
+ the_info = new_info
+ }
+ }
+
+ def update_rendering(r: Isabelle_Rendering, range: Text.Range)
+ { update(rendering(r)(range)) }
+
+ def reset { update(None) }
+ }
+
+ // owned by Swing thread
+
+ private var control: Boolean = false
+
+ private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
+ private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
+ private val active_areas = List(highlight_area, hyperlink_area)
+ private def active_reset(): Unit = active_areas.foreach(_.reset)
+
+ private val focus_listener = new FocusAdapter {
+ override def focusLost(e: FocusEvent) { active_reset() }
+ }
+
+ private val window_listener = new WindowAdapter {
+ override def windowIconified(e: WindowEvent) { active_reset() }
+ override def windowDeactivated(e: WindowEvent) { active_reset() }
+ }
+
+ private val mouse_listener = new MouseAdapter {
+ override def mouseClicked(e: MouseEvent) {
+ hyperlink_area.info match {
+ case Some(Text.Info(range, link)) => link.follow(view)
+ case None =>
+ }
+ }
+ }
+
+ private val mouse_motion_listener = new MouseMotionAdapter {
+ override def mouseMoved(e: MouseEvent) {
+ control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
+ if (control && !buffer.isLoading) {
+ JEdit_Lib.buffer_lock(buffer) {
+ val rendering = get_rendering()
+ val mouse_offset = text_area.xyToOffset(e.getX(), e.getY())
+ val mouse_range = JEdit_Lib.point_range(buffer, mouse_offset)
+ active_areas.foreach(_.update_rendering(rendering, mouse_range))
+ }
+ }
+ else active_reset()
+ }
+ }
+
+
+ /* tooltips */
+
+ private val tooltip_painter = new TextAreaExtension
+ {
+ override def getToolTipText(x: Int, y: Int): String =
+ {
+ robust_body(null: String) {
+ val rendering = get_rendering()
+ val offset = text_area.xyToOffset(x, y)
+ val range = Text.Range(offset, offset + 1)
+ val tip =
+ if (control) rendering.tooltip(range)
+ else rendering.tooltip_message(range)
+ tip.map(Isabelle.tooltip(_)) getOrElse null
+ }
+ }
}
@@ -227,7 +331,7 @@
val screen_line = first_line + i
val chunks = text_area.getChunksOfScreenLine(screen_line)
if (chunks != null) {
- val line_start = text_area.getBuffer.getLineStartOffset(line)
+ val line_start = buffer.getLineStartOffset(line)
gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
@@ -267,7 +371,7 @@
// highlight range -- potentially from other snapshot
for {
- info <- doc_view.highlight_info()
+ info <- highlight_area.info
Text.Info(range, color) <- info.try_restrict(line_range)
r <- JEdit_Lib.gfx_range(text_area, range)
} {
@@ -277,7 +381,7 @@
// hyperlink range -- potentially from other snapshot
for {
- info <- doc_view.hyperlink_info()
+ info <- hyperlink_area.info
Text.Info(range, _) <- info.try_restrict(line_range)
r <- JEdit_Lib.gfx_range(text_area, range)
} {
@@ -339,6 +443,7 @@
{
val painter = text_area.getPainter
painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
+ painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
@@ -349,11 +454,19 @@
painter.addExtension(500, foreground_painter)
painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
painter.removeExtension(orig_text_painter)
+ painter.addMouseListener(mouse_listener)
+ painter.addMouseMotionListener(mouse_motion_listener)
+ text_area.addFocusListener(focus_listener)
+ view.addWindowListener(window_listener)
}
def deactivate()
{
val painter = text_area.getPainter
+ view.removeWindowListener(window_listener)
+ text_area.removeFocusListener(focus_listener)
+ painter.removeMouseMotionListener(mouse_motion_listener)
+ painter.removeMouseListener(mouse_listener)
painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
painter.removeExtension(reset_state)
painter.removeExtension(foreground_painter)
@@ -364,6 +477,7 @@
painter.removeExtension(before_caret_painter1)
painter.removeExtension(text_painter)
painter.removeExtension(background_painter)
+ painter.removeExtension(tooltip_painter)
painter.removeExtension(set_state)
}
}
--- a/src/Tools/jEdit/src/text_overview.scala Mon Sep 17 18:14:54 2012 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala Mon Sep 17 20:23:25 2012 +0200
@@ -65,7 +65,7 @@
super.paintComponent(gfx)
Swing_Thread.assert()
- doc_view.robust_body(()) {
+ doc_view.text_area_painter.robust_body(()) {
JEdit_Lib.buffer_lock(buffer) {
val snapshot = doc_view.model.snapshot()