tuned signature -- more general Text_Area_Painter operations;
authorwenzelm
Mon Sep 17 20:23:25 2012 +0200 (2012-09-17)
changeset 4941034acbcc33adf
parent 49409 7140a738aa49
child 49411 1da54e9bda68
tuned signature -- more general Text_Area_Painter operations;
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/text_area_painter.scala
src/Tools/jEdit/src/text_overview.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Sep 17 18:14:54 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Sep 17 20:23:25 2012 +0200
     1.3 @@ -17,13 +17,9 @@
     1.4  import java.lang.System
     1.5  import java.text.BreakIterator
     1.6  import java.awt.{Color, Graphics2D, Point}
     1.7 -import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
     1.8 -  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
     1.9  import javax.swing.event.{CaretListener, CaretEvent}
    1.10  
    1.11 -import org.gjt.sp.util.Log
    1.12 -
    1.13 -import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
    1.14 +import org.gjt.sp.jedit.{jEdit, Debug}
    1.15  import org.gjt.sp.jedit.gui.RolloverButton
    1.16  import org.gjt.sp.jedit.options.GutterOptionPane
    1.17  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    1.18 @@ -72,22 +68,6 @@
    1.19    private val session = model.session
    1.20  
    1.21  
    1.22 -  /* robust extension body */
    1.23 -
    1.24 -  def robust_body[A](default: A)(body: => A): A =
    1.25 -  {
    1.26 -    try {
    1.27 -      Swing_Thread.require()
    1.28 -      if (model.buffer == text_area.getBuffer) body
    1.29 -      else {
    1.30 -        Log.log(Log.ERROR, this, ERROR("Inconsistent document model"))
    1.31 -        default
    1.32 -      }
    1.33 -    }
    1.34 -    catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
    1.35 -  }
    1.36 -
    1.37 -
    1.38    /* perspective */
    1.39  
    1.40    def perspective(): Text.Perspective =
    1.41 @@ -117,97 +97,12 @@
    1.42    }
    1.43  
    1.44  
    1.45 -  /* active areas within the text */
    1.46 -
    1.47 -  private class Active_Area[A](
    1.48 -    rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
    1.49 -  {
    1.50 -    private var the_info: Option[Text.Info[A]] = None
    1.51 -
    1.52 -    def info: Option[Text.Info[A]] = the_info
    1.53 -
    1.54 -    def update(new_info: Option[Text.Info[A]])
    1.55 -    {
    1.56 -      val old_info = the_info
    1.57 -      if (new_info != old_info) {
    1.58 -        for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
    1.59 -          JEdit_Lib.invalidate_range(text_area, range)
    1.60 -        the_info = new_info
    1.61 -      }
    1.62 -    }
    1.63 -
    1.64 -    def update_rendering(r: Isabelle_Rendering, range: Text.Range)
    1.65 -    { update(rendering(r)(range)) }
    1.66 -
    1.67 -    def reset { update(None) }
    1.68 -  }
    1.69 -
    1.70 -  // owned by Swing thread
    1.71 -
    1.72 -  private var control: Boolean = false
    1.73 -
    1.74 -  private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
    1.75 -  def highlight_info(): Option[Text.Info[Color]] = highlight_area.info
    1.76 -
    1.77 -  private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
    1.78 -  def hyperlink_info(): Option[Text.Info[Hyperlink]] = hyperlink_area.info
    1.79 -
    1.80 -  private val active_areas = List(highlight_area, hyperlink_area)
    1.81 -  private def active_reset(): Unit = active_areas.foreach(_.reset)
    1.82 -
    1.83 -  private val focus_listener = new FocusAdapter {
    1.84 -    override def focusLost(e: FocusEvent) { active_reset() }
    1.85 -  }
    1.86 -
    1.87 -  private val window_listener = new WindowAdapter {
    1.88 -    override def windowIconified(e: WindowEvent) { active_reset() }
    1.89 -    override def windowDeactivated(e: WindowEvent) { active_reset() }
    1.90 -  }
    1.91 -
    1.92 -  private val mouse_listener = new MouseAdapter {
    1.93 -    override def mouseClicked(e: MouseEvent) {
    1.94 -      hyperlink_area.info match {
    1.95 -        case Some(Text.Info(range, link)) => link.follow(text_area.getView)
    1.96 -        case None =>
    1.97 -      }
    1.98 -    }
    1.99 -  }
   1.100 -
   1.101 -  private val mouse_motion_listener = new MouseMotionAdapter {
   1.102 -    override def mouseMoved(e: MouseEvent) {
   1.103 -      control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
   1.104 -      if (control && model.buffer.isLoaded) {
   1.105 -        JEdit_Lib.buffer_lock(model.buffer) {
   1.106 -          val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
   1.107 -          val mouse_range =
   1.108 -            JEdit_Lib.point_range(model.buffer, text_area.xyToOffset(e.getX(), e.getY()))
   1.109 -          active_areas.foreach(_.update_rendering(rendering, mouse_range))
   1.110 -        }
   1.111 -      }
   1.112 -      else active_reset()
   1.113 -    }
   1.114 -  }
   1.115 -
   1.116 -
   1.117    /* text area painting */
   1.118  
   1.119 -  private val text_area_painter = new Text_Area_Painter(this)
   1.120 +  def get_rendering(): Isabelle_Rendering =
   1.121 +    Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
   1.122  
   1.123 -  private val tooltip_painter = new TextAreaExtension
   1.124 -  {
   1.125 -    override def getToolTipText(x: Int, y: Int): String =
   1.126 -    {
   1.127 -      robust_body(null: String) {
   1.128 -        val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
   1.129 -        val offset = text_area.xyToOffset(x, y)
   1.130 -        val range = Text.Range(offset, offset + 1)
   1.131 -        val tip =
   1.132 -          if (control) rendering.tooltip(range)
   1.133 -          else rendering.tooltip_message(range)
   1.134 -        tip.map(Isabelle.tooltip(_)) getOrElse null
   1.135 -      }
   1.136 -    }
   1.137 -  }
   1.138 +  val text_area_painter = new Text_Area_Painter(text_area.getView, text_area, get_rendering _)
   1.139  
   1.140    private val gutter_painter = new TextAreaExtension
   1.141    {
   1.142 @@ -215,7 +110,7 @@
   1.143        first_line: Int, last_line: Int, physical_lines: Array[Int],
   1.144        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   1.145      {
   1.146 -      robust_body(()) {
   1.147 +      text_area_painter.robust_body(()) {
   1.148          Swing_Thread.assert()
   1.149  
   1.150          val gutter = text_area.getGutter
   1.151 @@ -226,7 +121,7 @@
   1.152          if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
   1.153            val buffer = model.buffer
   1.154            JEdit_Lib.buffer_lock(buffer) {
   1.155 -            val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
   1.156 +            val rendering = get_rendering()
   1.157  
   1.158              for (i <- 0 until physical_lines.length) {
   1.159                if (physical_lines(i) != -1) {
   1.160 @@ -328,14 +223,10 @@
   1.161    private def activate()
   1.162    {
   1.163      val painter = text_area.getPainter
   1.164 +
   1.165      painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
   1.166 -    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
   1.167      text_area_painter.activate()
   1.168      text_area.getGutter.addExtension(gutter_painter)
   1.169 -    text_area.addFocusListener(focus_listener)
   1.170 -    text_area.getView.addWindowListener(window_listener)
   1.171 -    painter.addMouseListener(mouse_listener)
   1.172 -    painter.addMouseMotionListener(mouse_motion_listener)
   1.173      text_area.addCaretListener(caret_listener)
   1.174      text_area.addLeftOfScrollBar(overview)
   1.175      session.raw_edits += main_actor
   1.176 @@ -345,17 +236,13 @@
   1.177    private def deactivate()
   1.178    {
   1.179      val painter = text_area.getPainter
   1.180 +
   1.181      session.raw_edits -= main_actor
   1.182      session.commands_changed -= main_actor
   1.183 -    text_area.removeFocusListener(focus_listener)
   1.184 -    text_area.getView.removeWindowListener(window_listener)
   1.185 -    painter.removeMouseMotionListener(mouse_motion_listener)
   1.186 -    painter.removeMouseListener(mouse_listener)
   1.187      text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
   1.188      text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
   1.189      text_area.getGutter.removeExtension(gutter_painter)
   1.190      text_area_painter.deactivate()
   1.191 -    painter.removeExtension(tooltip_painter)
   1.192      painter.removeExtension(update_perspective)
   1.193    }
   1.194  }
     2.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Mon Sep 17 18:14:54 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Sep 17 20:23:25 2012 +0200
     2.3 @@ -47,7 +47,7 @@
     2.4          val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get
     2.5          Document_View(view.getTextArea) match {
     2.6            case Some(doc_view) =>
     2.7 -            doc_view.robust_body() {
     2.8 +            doc_view.text_area_painter.robust_body() {
     2.9                val cmd = current_state.command
    2.10                val model = doc_view.model
    2.11                val buffer = model.buffer
     3.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Mon Sep 17 18:14:54 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Mon Sep 17 20:23:25 2012 +0200
     3.3 @@ -9,21 +9,38 @@
     3.4  
     3.5  import isabelle._
     3.6  
     3.7 -import java.awt.{Graphics2D, Shape}
     3.8 +import java.awt.{Graphics2D, Shape, Window, Color}
     3.9 +import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
    3.10 +  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
    3.11  import java.awt.font.TextAttribute
    3.12  import java.text.AttributedString
    3.13  import java.util.ArrayList
    3.14  
    3.15 -import org.gjt.sp.jedit.Debug
    3.16 +import org.gjt.sp.util.Log
    3.17 +import org.gjt.sp.jedit.{OperatingSystem, Debug, View}
    3.18  import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
    3.19 -import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
    3.20 +import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
    3.21 +
    3.22 +
    3.23 +class Text_Area_Painter(view: View, text_area: TextArea, get_rendering: () => Isabelle_Rendering)
    3.24 +{
    3.25 +  private val buffer = text_area.getBuffer
    3.26  
    3.27  
    3.28 -class Text_Area_Painter(doc_view: Document_View)
    3.29 -{
    3.30 -  private val model = doc_view.model
    3.31 -  private val buffer = model.buffer
    3.32 -  private val text_area = doc_view.text_area
    3.33 +  /* robust extension body */
    3.34 +
    3.35 +  def robust_body[A](default: A)(body: => A): A =
    3.36 +  {
    3.37 +    try {
    3.38 +      Swing_Thread.require()
    3.39 +      if (buffer == text_area.getBuffer) body
    3.40 +      else {
    3.41 +        Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
    3.42 +        default
    3.43 +      }
    3.44 +    }
    3.45 +    catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
    3.46 +  }
    3.47  
    3.48  
    3.49    /* original painters */
    3.50 @@ -52,7 +69,7 @@
    3.51        first_line: Int, last_line: Int, physical_lines: Array[Int],
    3.52        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    3.53      {
    3.54 -      painter_rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
    3.55 +      painter_rendering = get_rendering()
    3.56        painter_clip = gfx.getClip
    3.57      }
    3.58    }
    3.59 @@ -70,7 +87,94 @@
    3.60  
    3.61    private def robust_rendering(body: Isabelle_Rendering => Unit)
    3.62    {
    3.63 -    doc_view.robust_body(()) { body(painter_rendering) }
    3.64 +    robust_body(()) { body(painter_rendering) }
    3.65 +  }
    3.66 +
    3.67 +
    3.68 +  /* active areas within the text */
    3.69 +
    3.70 +  private class Active_Area[A](
    3.71 +    rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
    3.72 +  {
    3.73 +    private var the_info: Option[Text.Info[A]] = None
    3.74 +
    3.75 +    def info: Option[Text.Info[A]] = the_info
    3.76 +
    3.77 +    def update(new_info: Option[Text.Info[A]])
    3.78 +    {
    3.79 +      val old_info = the_info
    3.80 +      if (new_info != old_info) {
    3.81 +        for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
    3.82 +          JEdit_Lib.invalidate_range(text_area, range)
    3.83 +        the_info = new_info
    3.84 +      }
    3.85 +    }
    3.86 +
    3.87 +    def update_rendering(r: Isabelle_Rendering, range: Text.Range)
    3.88 +    { update(rendering(r)(range)) }
    3.89 +
    3.90 +    def reset { update(None) }
    3.91 +  }
    3.92 +
    3.93 +  // owned by Swing thread
    3.94 +
    3.95 +  private var control: Boolean = false
    3.96 +
    3.97 +  private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
    3.98 +  private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
    3.99 +  private val active_areas = List(highlight_area, hyperlink_area)
   3.100 +  private def active_reset(): Unit = active_areas.foreach(_.reset)
   3.101 +
   3.102 +  private val focus_listener = new FocusAdapter {
   3.103 +    override def focusLost(e: FocusEvent) { active_reset() }
   3.104 +  }
   3.105 +
   3.106 +  private val window_listener = new WindowAdapter {
   3.107 +    override def windowIconified(e: WindowEvent) { active_reset() }
   3.108 +    override def windowDeactivated(e: WindowEvent) { active_reset() }
   3.109 +  }
   3.110 +
   3.111 +  private val mouse_listener = new MouseAdapter {
   3.112 +    override def mouseClicked(e: MouseEvent) {
   3.113 +      hyperlink_area.info match {
   3.114 +        case Some(Text.Info(range, link)) => link.follow(view)
   3.115 +        case None =>
   3.116 +      }
   3.117 +    }
   3.118 +  }
   3.119 +
   3.120 +  private val mouse_motion_listener = new MouseMotionAdapter {
   3.121 +    override def mouseMoved(e: MouseEvent) {
   3.122 +      control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
   3.123 +      if (control && !buffer.isLoading) {
   3.124 +        JEdit_Lib.buffer_lock(buffer) {
   3.125 +          val rendering = get_rendering()
   3.126 +          val mouse_offset = text_area.xyToOffset(e.getX(), e.getY())
   3.127 +          val mouse_range = JEdit_Lib.point_range(buffer, mouse_offset)
   3.128 +          active_areas.foreach(_.update_rendering(rendering, mouse_range))
   3.129 +        }
   3.130 +      }
   3.131 +      else active_reset()
   3.132 +    }
   3.133 +  }
   3.134 +
   3.135 +
   3.136 +  /* tooltips */
   3.137 +
   3.138 +  private val tooltip_painter = new TextAreaExtension
   3.139 +  {
   3.140 +    override def getToolTipText(x: Int, y: Int): String =
   3.141 +    {
   3.142 +      robust_body(null: String) {
   3.143 +        val rendering = get_rendering()
   3.144 +        val offset = text_area.xyToOffset(x, y)
   3.145 +        val range = Text.Range(offset, offset + 1)
   3.146 +        val tip =
   3.147 +          if (control) rendering.tooltip(range)
   3.148 +          else rendering.tooltip_message(range)
   3.149 +        tip.map(Isabelle.tooltip(_)) getOrElse null
   3.150 +      }
   3.151 +    }
   3.152    }
   3.153  
   3.154  
   3.155 @@ -227,7 +331,7 @@
   3.156              val screen_line = first_line + i
   3.157              val chunks = text_area.getChunksOfScreenLine(screen_line)
   3.158              if (chunks != null) {
   3.159 -              val line_start = text_area.getBuffer.getLineStartOffset(line)
   3.160 +              val line_start = buffer.getLineStartOffset(line)
   3.161                gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
   3.162                val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
   3.163                gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
   3.164 @@ -267,7 +371,7 @@
   3.165  
   3.166              // highlight range -- potentially from other snapshot
   3.167              for {
   3.168 -              info <- doc_view.highlight_info()
   3.169 +              info <- highlight_area.info
   3.170                Text.Info(range, color) <- info.try_restrict(line_range)
   3.171                r <- JEdit_Lib.gfx_range(text_area, range)
   3.172              } {
   3.173 @@ -277,7 +381,7 @@
   3.174  
   3.175              // hyperlink range -- potentially from other snapshot
   3.176              for {
   3.177 -              info <- doc_view.hyperlink_info()
   3.178 +              info <- hyperlink_area.info
   3.179                Text.Info(range, _) <- info.try_restrict(line_range)
   3.180                r <- JEdit_Lib.gfx_range(text_area, range)
   3.181              } {
   3.182 @@ -339,6 +443,7 @@
   3.183    {
   3.184      val painter = text_area.getPainter
   3.185      painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
   3.186 +    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
   3.187      painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   3.188      painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
   3.189      painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
   3.190 @@ -349,11 +454,19 @@
   3.191      painter.addExtension(500, foreground_painter)
   3.192      painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
   3.193      painter.removeExtension(orig_text_painter)
   3.194 +    painter.addMouseListener(mouse_listener)
   3.195 +    painter.addMouseMotionListener(mouse_motion_listener)
   3.196 +    text_area.addFocusListener(focus_listener)
   3.197 +    view.addWindowListener(window_listener)
   3.198    }
   3.199  
   3.200    def deactivate()
   3.201    {
   3.202      val painter = text_area.getPainter
   3.203 +    view.removeWindowListener(window_listener)
   3.204 +    text_area.removeFocusListener(focus_listener)
   3.205 +    painter.removeMouseMotionListener(mouse_motion_listener)
   3.206 +    painter.removeMouseListener(mouse_listener)
   3.207      painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
   3.208      painter.removeExtension(reset_state)
   3.209      painter.removeExtension(foreground_painter)
   3.210 @@ -364,6 +477,7 @@
   3.211      painter.removeExtension(before_caret_painter1)
   3.212      painter.removeExtension(text_painter)
   3.213      painter.removeExtension(background_painter)
   3.214 +    painter.removeExtension(tooltip_painter)
   3.215      painter.removeExtension(set_state)
   3.216    }
   3.217  }
     4.1 --- a/src/Tools/jEdit/src/text_overview.scala	Mon Sep 17 18:14:54 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/text_overview.scala	Mon Sep 17 20:23:25 2012 +0200
     4.3 @@ -65,7 +65,7 @@
     4.4      super.paintComponent(gfx)
     4.5      Swing_Thread.assert()
     4.6  
     4.7 -    doc_view.robust_body(()) {
     4.8 +    doc_view.text_area_painter.robust_body(()) {
     4.9        JEdit_Lib.buffer_lock(buffer) {
    4.10          val snapshot = doc_view.model.snapshot()
    4.11