flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);
authorwenzelm
Fri Jun 17 13:55:53 2011 +0200 (2011-06-17)
changeset 434196ed49c52d463
parent 43418 c69e9fbb81a8
child 43420 a26e514c92b2
flush snapshot on falling edge of is_outdated -- recover effect of former buffer.propertiesChanged on text area (cf. f0770743b7ec);
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/text_area_painter.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Jun 17 00:10:39 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Jun 17 13:55:53 2011 +0200
     1.3 @@ -69,7 +69,7 @@
     1.4    private val session = model.session
     1.5  
     1.6  
     1.7 -  /** robust extension body **/
     1.8 +  /* robust extension body */
     1.9  
    1.10    def robust_body[A](default: A)(body: => A): A =
    1.11    {
    1.12 @@ -85,8 +85,6 @@
    1.13    }
    1.14  
    1.15  
    1.16 -  /** token handling **/
    1.17 -
    1.18    /* visible line ranges */
    1.19  
    1.20    // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
    1.21 @@ -112,6 +110,31 @@
    1.22    }
    1.23  
    1.24  
    1.25 +  /* snapshot */
    1.26 +
    1.27 +  // owned by Swing thread
    1.28 +  @volatile private var was_outdated = false
    1.29 +  @volatile private var was_updated = false
    1.30 +
    1.31 +  def update_snapshot(): Document.Snapshot =
    1.32 +  {
    1.33 +    Swing_Thread.require()
    1.34 +    val snapshot = model.snapshot()
    1.35 +    was_updated = was_outdated && !snapshot.is_outdated
    1.36 +    was_outdated = was_outdated || snapshot.is_outdated
    1.37 +    snapshot
    1.38 +  }
    1.39 +
    1.40 +  def flush_snapshot(): (Boolean, Document.Snapshot) =
    1.41 +  {
    1.42 +    Swing_Thread.require()
    1.43 +    val snapshot = update_snapshot()
    1.44 +    val updated = was_updated
    1.45 +    if (updated) { was_outdated = false; was_updated = false }
    1.46 +    (updated, snapshot)
    1.47 +  }
    1.48 +
    1.49 +
    1.50    /* HTML popups */
    1.51  
    1.52    private var html_popup: Option[Popup] = None
    1.53 @@ -196,7 +219,7 @@
    1.54        if (!model.buffer.isLoaded) exit_control()
    1.55        else
    1.56          Isabelle.swing_buffer_lock(model.buffer) {
    1.57 -          val snapshot = model.snapshot
    1.58 +          val snapshot = update_snapshot()
    1.59  
    1.60            if (control) init_popup(snapshot, x, y)
    1.61  
    1.62 @@ -217,7 +240,7 @@
    1.63      override def getToolTipText(x: Int, y: Int): String =
    1.64      {
    1.65        robust_body(null: String) {
    1.66 -        val snapshot = model.snapshot()
    1.67 +        val snapshot = update_snapshot()
    1.68          val offset = text_area.xyToOffset(x, y)
    1.69          if (control) {
    1.70            snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
    1.71 @@ -249,14 +272,14 @@
    1.72          val width = GutterOptionPane.getSelectionAreaWidth
    1.73          val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
    1.74          val FOLD_MARKER_SIZE = 12
    1.75 -  
    1.76 +
    1.77          if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
    1.78            Isabelle.swing_buffer_lock(model.buffer) {
    1.79 -            val snapshot = model.snapshot()
    1.80 +            val snapshot = update_snapshot()
    1.81              for (i <- 0 until physical_lines.length) {
    1.82                if (physical_lines(i) != -1) {
    1.83                  val line_range = proper_line_range(start(i), end(i))
    1.84 -  
    1.85 +
    1.86                  // gutter icons
    1.87                  val icons =
    1.88                    (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
    1.89 @@ -284,7 +307,7 @@
    1.90    def selected_command(): Option[Command] =
    1.91    {
    1.92      Swing_Thread.require()
    1.93 -    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
    1.94 +    update_snapshot().node.proper_command_at(text_area.getCaretPosition)
    1.95    }
    1.96  
    1.97    private val caret_listener = new CaretListener {
    1.98 @@ -331,7 +354,7 @@
    1.99  
   1.100        val buffer = model.buffer
   1.101        Isabelle.buffer_lock(buffer) {
   1.102 -        val snapshot = model.snapshot()
   1.103 +        val snapshot = update_snapshot()
   1.104  
   1.105          def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
   1.106          {
   1.107 @@ -372,22 +395,26 @@
   1.108          case Session.Commands_Changed(changed) =>
   1.109            val buffer = model.buffer
   1.110            Isabelle.swing_buffer_lock(buffer) {
   1.111 -            val snapshot = model.snapshot()
   1.112 +            val (updated, snapshot) = flush_snapshot()
   1.113 +            val visible_range = screen_lines_range()
   1.114  
   1.115 -            if (changed.exists(snapshot.node.commands.contains))
   1.116 +            if (updated || changed.exists(snapshot.node.commands.contains))
   1.117                overview.repaint()
   1.118  
   1.119 -            val visible_range = screen_lines_range()
   1.120 -            val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
   1.121 -            if (visible_cmds.exists(changed)) {
   1.122 -              for {
   1.123 -                line <- 0 until text_area.getVisibleLines
   1.124 -                val start = text_area.getScreenLineStartOffset(line) if start >= 0
   1.125 -                val end = text_area.getScreenLineEndOffset(line) if end >= 0
   1.126 -                val range = proper_line_range(start, end)
   1.127 -                val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
   1.128 -                if line_cmds.exists(changed)
   1.129 -              } text_area.invalidateScreenLineRange(line, line)
   1.130 +            if (updated) invalidate_line_range(visible_range)
   1.131 +            else {
   1.132 +              val visible_cmds =
   1.133 +                snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
   1.134 +              if (visible_cmds.exists(changed)) {
   1.135 +                for {
   1.136 +                  line <- 0 until text_area.getVisibleLines
   1.137 +                  val start = text_area.getScreenLineStartOffset(line) if start >= 0
   1.138 +                  val end = text_area.getScreenLineEndOffset(line) if end >= 0
   1.139 +                  val range = proper_line_range(start, end)
   1.140 +                  val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
   1.141 +                  if line_cmds.exists(changed)
   1.142 +                } text_area.invalidateScreenLineRange(line, line)
   1.143 +              }
   1.144              }
   1.145            }
   1.146  
     2.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Fri Jun 17 00:10:39 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Jun 17 13:55:53 2011 +0200
     2.3 @@ -34,7 +34,7 @@
     2.4          Document_View(view.getTextArea) match {
     2.5            case Some(doc_view) =>
     2.6              val cmd = current_command.get
     2.7 -            val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get
     2.8 +            val start_ofs = doc_view.update_snapshot().node.command_start(cmd).get
     2.9              val buffer = view.getBuffer
    2.10              buffer.beginCompoundEdit()
    2.11              buffer.remove(start_ofs, cmd.length)
    2.12 @@ -83,7 +83,7 @@
    2.13          case Some(doc_view) =>
    2.14            current_command match {
    2.15              case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
    2.16 -              val snapshot = doc_view.model.snapshot()
    2.17 +              val snapshot = doc_view.update_snapshot()
    2.18                val filtered_results =
    2.19                  snapshot.state(cmd).results.iterator.map(_._2) filter {
    2.20                    case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing  // FIXME not scalable
     3.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Fri Jun 17 00:10:39 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Fri Jun 17 13:55:53 2011 +0200
     3.3 @@ -53,7 +53,7 @@
     3.4        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     3.5      {
     3.6        doc_view.robust_body(()) {
     3.7 -        painter_snapshot = model.snapshot()
     3.8 +        painter_snapshot = doc_view.update_snapshot()
     3.9          painter_clip = gfx.getClip
    3.10        }
    3.11      }