1.1 --- a/src/Pure/System/session.scala	Mon Mar 19 21:52:09 2012 +0100
     1.2 +++ b/src/Pure/System/session.scala	Mon Mar 19 23:08:27 2012 +0100
     1.3 @@ -24,7 +24,8 @@
     1.4    //{{{
     1.5    case object Global_Settings
     1.6    case object Caret_Focus
     1.7 -  case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
     1.8 +  case class Commands_Changed(
     1.9 +    assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
    1.10  
    1.11    sealed abstract class Phase
    1.12    case object Inactive extends Phase
    1.13 @@ -227,9 +228,9 @@
    1.14  
    1.15      object delay_commands_changed
    1.16      {
    1.17 +      private var changed_assignment: Boolean = false
    1.18        private var changed_nodes: Set[Document.Node.Name] = Set.empty
    1.19        private var changed_commands: Set[Command] = Set.empty
    1.20 -      private def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
    1.21  
    1.22        private var flush_time: Option[Long] = None
    1.23  
    1.24 @@ -241,17 +242,22 @@
    1.25  
    1.26        def flush()
    1.27        {
    1.28 -        if (changed)
    1.29 -          commands_changed_buffer ! Session.Commands_Changed(changed_nodes, changed_commands)
    1.30 +        if (changed_assignment || !changed_nodes.isEmpty || !changed_commands.isEmpty)
    1.31 +          commands_changed_buffer !
    1.32 +            Session.Commands_Changed(changed_assignment, changed_nodes, changed_commands)
    1.33 +        changed_assignment = false
    1.34          changed_nodes = Set.empty
    1.35          changed_commands = Set.empty
    1.36          flush_time = None
    1.37        }
    1.38  
    1.39 -      def invoke(command: Command)
    1.40 +      def invoke(assign: Boolean, commands: List[Command])
    1.41        {
    1.42 -        changed_nodes += command.node_name
    1.43 -        changed_commands += command
    1.44 +        changed_assignment |= assign
    1.45 +        for (command <- commands) {
    1.46 +          changed_nodes += command.node_name
    1.47 +          changed_commands += command
    1.48 +        }
    1.49          val now = System.currentTimeMillis()
    1.50          flush_time match {
    1.51            case None => flush_time = Some(now + output_delay.ms)
    1.52 @@ -304,22 +310,16 @@
    1.53      /* exec state assignment */
    1.54  
    1.55      def handle_assign(id: Document.Version_ID, assign: Document.Assign)
    1.56 -    //{{{
    1.57      {
    1.58        val cmds = global_state >>> (_.assign(id, assign))
    1.59 -      for (cmd <- cmds) delay_commands_changed.invoke(cmd)
    1.60 +      delay_commands_changed.invoke(true, cmds)
    1.61      }
    1.62 -    //}}}
    1.63  
    1.64  
    1.65      /* removed versions */
    1.66  
    1.67 -    def handle_removed(removed: List[Document.Version_ID])
    1.68 -    //{{{
    1.69 -    {
    1.70 +    def handle_removed(removed: List[Document.Version_ID]): Unit =
    1.71        global_state >> (_.removed_versions(removed))
    1.72 -    }
    1.73 -    //}}}
    1.74  
    1.75  
    1.76      /* resulting changes */
    1.77 @@ -367,7 +367,7 @@
    1.78          case Position.Id(state_id) if !output.is_protocol =>
    1.79            try {
    1.80              val st = global_state >>> (_.accumulate(state_id, output.message))
    1.81 -            delay_commands_changed.invoke(st.command)
    1.82 +            delay_commands_changed.invoke(false, List(st.command))
    1.83            }
    1.84            catch {
    1.85              case _: Document.State.Fail => bad_output(output)

     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Mar 19 21:52:09 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Mar 19 23:08:27 2012 +0100
     2.3 @@ -144,31 +144,6 @@
     2.4    }
     2.5  
     2.6  
     2.7 -  /* snapshot */
     2.8 -
     2.9 -  // owned by Swing thread
    2.10 -  @volatile private var was_outdated = false
    2.11 -  @volatile private var was_updated = false
    2.12 -
    2.13 -  def update_snapshot(): Document.Snapshot =
    2.14 -  {
    2.15 -    Swing_Thread.require()
    2.16 -    val snapshot = model.snapshot()
    2.17 -    was_updated &&= !snapshot.is_outdated
    2.18 -    was_outdated ||= snapshot.is_outdated
    2.19 -    snapshot
    2.20 -  }
    2.21 -
    2.22 -  def flush_snapshot(): (Boolean, Document.Snapshot) =
    2.23 -  {
    2.24 -    Swing_Thread.require()
    2.25 -    val snapshot = update_snapshot()
    2.26 -    val updated = was_updated
    2.27 -    if (updated) { was_outdated = false; was_updated = false }
    2.28 -    (updated, snapshot)
    2.29 -  }
    2.30 -
    2.31 -
    2.32    /* HTML popups */
    2.33  
    2.34    private var html_popup: Option[Popup] = None
    2.35 @@ -242,7 +217,7 @@
    2.36        if (!model.buffer.isLoaded) exit_control()
    2.37        else
    2.38          Isabelle.buffer_lock(model.buffer) {
    2.39 -          val snapshot = update_snapshot()
    2.40 +          val snapshot = model.snapshot()
    2.41  
    2.42            if (control) init_popup(snapshot, x, y)
    2.43  
    2.44 @@ -268,7 +243,7 @@
    2.45      override def getToolTipText(x: Int, y: Int): String =
    2.46      {
    2.47        robust_body(null: String) {
    2.48 -        val snapshot = update_snapshot()
    2.49 +        val snapshot = model.snapshot()
    2.50          val offset = text_area.xyToOffset(x, y)
    2.51          val range = Text.Range(offset, offset + 1)
    2.52          val tip =
    2.53 @@ -295,7 +270,7 @@
    2.54  
    2.55          if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
    2.56            Isabelle.buffer_lock(model.buffer) {
    2.57 -            val snapshot = update_snapshot()
    2.58 +            val snapshot = model.snapshot()
    2.59              for (i <- 0 until physical_lines.length) {
    2.60                if (physical_lines(i) != -1) {
    2.61                  val line_range = proper_line_range(start(i), end(i))
    2.62 @@ -340,7 +315,7 @@
    2.63    def selected_command(): Option[Command] =
    2.64    {
    2.65      Swing_Thread.require()
    2.66 -    update_snapshot().node.command_at(text_area.getCaretPosition).map(_._1)
    2.67 +    model.snapshot().node.command_at(text_area.getCaretPosition).map(_._1)
    2.68    }
    2.69  
    2.70    private val delay_caret_update =
    2.71 @@ -372,16 +347,16 @@
    2.72            Swing_Thread.later {
    2.73              Isabelle.buffer_lock(buffer) {
    2.74                if (model.buffer == text_area.getBuffer) {
    2.75 -                val (updated, snapshot) = flush_snapshot()
    2.76 +                val snapshot = model.snapshot()
    2.77  
    2.78 -                if (updated ||
    2.79 +                if (changed.assignment ||
    2.80                      (changed.nodes.contains(model.name) &&
    2.81                       changed.commands.exists(snapshot.node.commands.contains)))
    2.82                    overview.delay_repaint(true)
    2.83  
    2.84                  visible_range() match {
    2.85                    case Some(visible) =>
    2.86 -                    if (updated) invalidate_range(visible)
    2.87 +                    if (changed.assignment) invalidate_range(visible)
    2.88                      else {
    2.89                        val visible_cmds =
    2.90                          snapshot.node.command_range(snapshot.revert(visible)).map(_._1)

     3.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Mon Mar 19 21:52:09 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Mar 19 23:08:27 2012 +0100
     3.3 @@ -35,7 +35,7 @@
     3.4          Document_View(view.getTextArea) match {
     3.5            case Some(doc_view) =>
     3.6              val cmd = current_command.get
     3.7 -            val start_ofs = doc_view.update_snapshot().node.command_start(cmd).get
     3.8 +            val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get
     3.9              val buffer = view.getBuffer
    3.10              buffer.beginCompoundEdit()
    3.11              buffer.remove(start_ofs, cmd.length)
    3.12 @@ -84,7 +84,7 @@
    3.13          case Some(doc_view) =>
    3.14            current_command match {
    3.15              case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
    3.16 -              val snapshot = doc_view.update_snapshot()
    3.17 +              val snapshot = doc_view.model.snapshot()
    3.18                val filtered_results =
    3.19                  snapshot.state.command_state(snapshot.version, cmd).results.iterator
    3.20                    .map(_._2).filter(

     4.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Mon Mar 19 21:52:09 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Mon Mar 19 23:08:27 2012 +0100
     4.3 @@ -84,7 +84,7 @@
     4.4        first_line: Int, last_line: Int, physical_lines: Array[Int],
     4.5        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     4.6      {
     4.7 -      painter_snapshot = doc_view.update_snapshot()
     4.8 +      painter_snapshot = model.snapshot()
     4.9        painter_clip = gfx.getClip
    4.10      }
    4.11    }

     5.1 --- a/src/Tools/jEdit/src/text_overview.scala	Mon Mar 19 21:52:09 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/text_overview.scala	Mon Mar 19 23:08:27 2012 +0100
     5.3 @@ -55,7 +55,7 @@
     5.4  
     5.5      doc_view.robust_body(()) {
     5.6        Isabelle.buffer_lock(buffer) {
     5.7 -        val snapshot = doc_view.update_snapshot()
     5.8 +        val snapshot = doc_view.model.snapshot()
     5.9  
    5.10          gfx.setColor(getBackground)
    5.11          gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)