1.1 --- a/src/Pure/PIDE/change.scala	Thu Aug 05 14:35:35 2010 +0200
     1.2 +++ b/src/Pure/PIDE/change.scala	Thu Aug 05 16:58:18 2010 +0200
     1.3 @@ -2,7 +2,7 @@
     1.4      Author:     Fabian Immler, TU Munich
     1.5      Author:     Makarius
     1.6  
     1.7 -Changes of plain text.
     1.8 +Changes of plain text, resulting in document edits.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12 @@ -11,14 +11,25 @@
    1.13  object Change
    1.14  {
    1.15    val init = new Change(Document.NO_ID, None, Nil, Future.value(Nil, Document.init))
    1.16 +
    1.17 +  abstract class Snapshot
    1.18 +  {
    1.19 +    val latest_version: Change
    1.20 +    val stable_version: Change
    1.21 +    val document: Document
    1.22 +    val node: Document.Node
    1.23 +    def is_outdated: Boolean = stable_version != latest_version
    1.24 +  }
    1.25  }
    1.26  
    1.27  class Change(
    1.28    val id: Document.Version_ID,
    1.29    val parent: Option[Change],
    1.30 -  val edits: List[Document.Node.Text_Edit],
    1.31 +  val edits: List[Document.Node_Text_Edit],
    1.32    val result: Future[(List[Document.Edit[Command]], Document)])
    1.33  {
    1.34 +  /* ancestor versions */
    1.35 +
    1.36    def ancestors: Iterator[Change] = new Iterator[Change]
    1.37    {
    1.38      private var state: Option[Change] = Some(Change.this)
    1.39 @@ -30,10 +41,10 @@
    1.40        }
    1.41    }
    1.42  
    1.43 -  def join_document: Document = result.join._2
    1.44 -  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
    1.45  
    1.46 -  def edit(session: Session, edits: List[Document.Node.Text_Edit]): Change =
    1.47 +  /* editing and state assignment */
    1.48 +
    1.49 +  def edit(session: Session, edits: List[Document.Node_Text_Edit]): Change =
    1.50    {
    1.51      val new_id = session.create_id()
    1.52      val result: Future[(List[Document.Edit[Command]], Document)] =
    1.53 @@ -44,4 +55,21 @@
    1.54        }
    1.55      new Change(new_id, Some(this), edits, result)
    1.56    }
    1.57 +
    1.58 +  def join_document: Document = result.join._2
    1.59 +  def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
    1.60 +
    1.61 +
    1.62 +  /* snapshot */
    1.63 +
    1.64 +  def snapshot(name: String): Change.Snapshot =
    1.65 +  {
    1.66 +    val latest = this
    1.67 +    new Change.Snapshot {
    1.68 +      val latest_version = latest
    1.69 +      val stable_version: Change = latest.ancestors.find(_.is_assigned).get
    1.70 +      val document: Document = stable_version.join_document
    1.71 +      val node: Document.Node = document.nodes(name)
    1.72 +    }
    1.73 +  }
    1.74  }
    1.75 \ No newline at end of file

     2.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 05 14:35:35 2010 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 05 16:58:18 2010 +0200
     2.3 @@ -23,15 +23,6 @@
     2.4    val NO_ID = ""
     2.5  
     2.6  
     2.7 -  /* nodes */
     2.8 -
     2.9 -  object Node { type Text_Edit = (String, List[isabelle.Text_Edit]) }  // FIXME None: remove
    2.10 -
    2.11 -  type Edit[C] =
    2.12 -   (String,  // node name
    2.13 -    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
    2.14 -
    2.15 -
    2.16    /* command start positions */
    2.17  
    2.18    def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
    2.19 @@ -45,21 +36,65 @@
    2.20    }
    2.21  
    2.22  
    2.23 +  /* named document nodes */
    2.24 +
    2.25 +  object Node
    2.26 +  {
    2.27 +    val empty: Node = new Node(Linear_Set())
    2.28 +  }
    2.29 +
    2.30 +  class Node(val commands: Linear_Set[Command])
    2.31 +  {
    2.32 +    /* command ranges */
    2.33 +
    2.34 +    def command_starts: Iterator[(Command, Int)] =
    2.35 +      Document.command_starts(commands.iterator)
    2.36 +
    2.37 +    def command_start(cmd: Command): Option[Int] =
    2.38 +      command_starts.find(_._1 == cmd).map(_._2)
    2.39 +
    2.40 +    def command_range(i: Int): Iterator[(Command, Int)] =
    2.41 +      command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
    2.42 +
    2.43 +    def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
    2.44 +      command_range(i) takeWhile { case (_, start) => start < j }
    2.45 +
    2.46 +    def command_at(i: Int): Option[(Command, Int)] =
    2.47 +    {
    2.48 +      val range = command_range(i)
    2.49 +      if (range.hasNext) Some(range.next) else None
    2.50 +    }
    2.51 +
    2.52 +    def proper_command_at(i: Int): Option[Command] =
    2.53 +      command_at(i) match {
    2.54 +        case Some((command, _)) =>
    2.55 +          commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
    2.56 +        case None => None
    2.57 +      }
    2.58 +  }
    2.59 +
    2.60 +
    2.61    /* initial document */
    2.62  
    2.63    val init: Document =
    2.64    {
    2.65 -    val doc = new Document(NO_ID, Map().withDefaultValue(Linear_Set()), Map())
    2.66 +    val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map())
    2.67      doc.assign_states(Nil)
    2.68      doc
    2.69    }
    2.70  
    2.71  
    2.72  
    2.73 -  /** document edits **/
    2.74 +  /** editing **/
    2.75 +
    2.76 +  type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
    2.77 +
    2.78 +  type Edit[C] =
    2.79 +   (String,  // node name
    2.80 +    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
    2.81  
    2.82    def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
    2.83 -      edits: List[Node.Text_Edit]): (List[Edit[Command]], Document) =
    2.84 +      edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
    2.85    {
    2.86      require(old_doc.assignment.is_finished)
    2.87  
    2.88 @@ -145,7 +180,7 @@
    2.89        var former_states = old_doc.assignment.join
    2.90  
    2.91        for ((name, text_edits) <- edits) {
    2.92 -        val commands0 = nodes(name)
    2.93 +        val commands0 = nodes(name).commands
    2.94          val commands1 = edit_text(text_edits, commands0)
    2.95          val commands2 = parse_spans(commands1)
    2.96  
    2.97 @@ -157,7 +192,7 @@
    2.98            inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
    2.99  
   2.100          doc_edits += (name -> Some(cmd_edits))
   2.101 -        nodes += (name -> commands2)
   2.102 +        nodes += (name -> new Node(commands2))
   2.103          former_states --= removed_commands
   2.104        }
   2.105        (doc_edits.toList, new Document(new_id, nodes, former_states))
   2.106 @@ -168,39 +203,9 @@
   2.107  
   2.108  class Document(
   2.109      val id: Document.Version_ID,
   2.110 -    val nodes: Map[String, Linear_Set[Command]],
   2.111 +    val nodes: Map[String, Document.Node],
   2.112      former_states: Map[Command, Command])  // FIXME !?
   2.113  {
   2.114 -  /* command ranges */
   2.115 -
   2.116 -  def commands(name: String): Linear_Set[Command] = nodes.get(name) getOrElse Linear_Set()
   2.117 -
   2.118 -  def command_starts(name: String): Iterator[(Command, Int)] =
   2.119 -    Document.command_starts(commands(name).iterator)
   2.120 -
   2.121 -  def command_start(name: String, cmd: Command): Option[Int] =
   2.122 -    command_starts(name).find(_._1 == cmd).map(_._2)
   2.123 -
   2.124 -  def command_range(name: String, i: Int): Iterator[(Command, Int)] =
   2.125 -    command_starts(name) dropWhile { case (cmd, start) => start + cmd.length <= i }
   2.126 -
   2.127 -  def command_range(name: String, i: Int, j: Int): Iterator[(Command, Int)] =
   2.128 -    command_range(name, i) takeWhile { case (_, start) => start < j }
   2.129 -
   2.130 -  def command_at(name: String, i: Int): Option[(Command, Int)] =
   2.131 -  {
   2.132 -    val range = command_range(name, i)
   2.133 -    if (range.hasNext) Some(range.next) else None
   2.134 -  }
   2.135 -
   2.136 -  def proper_command_at(name: String, i: Int): Option[Command] =
   2.137 -    command_at(name, i) match {
   2.138 -      case Some((command, _)) =>
   2.139 -        commands(name).reverse_iterator(command).find(cmd => !cmd.is_ignored)
   2.140 -      case None => None
   2.141 -    }
   2.142 -
   2.143 -
   2.144    /* command state assignment */
   2.145  
   2.146    val assignment = Future.promise[Map[Command, Command]]

     3.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 05 14:35:35 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Thu Aug 05 16:58:18 2010 +0200
     3.3 @@ -54,6 +54,7 @@
     3.4    }
     3.5  }
     3.6  
     3.7 +
     3.8  class Document_Model(val session: Session, val buffer: Buffer)
     3.9  {
    3.10    /* visible line end */
    3.11 @@ -77,7 +78,7 @@
    3.12    @volatile private var history = Change.init // owned by Swing thread
    3.13  
    3.14    def current_change(): Change = history
    3.15 -  def recent_document(): Document = current_change().ancestors.find(_.is_assigned).get.join_document
    3.16 +  def snapshot(): Change.Snapshot = current_change().snapshot(thy_name)
    3.17  
    3.18  
    3.19    /* transforming offsets */

     4.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Thu Aug 05 14:35:35 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Thu Aug 05 16:58:18 2010 +0200
     4.3 @@ -24,10 +24,11 @@
     4.4  
     4.5  object Document_View
     4.6  {
     4.7 -  def choose_color(document: Document, command: Command): Color =
     4.8 +  def choose_color(snapshot: Change.Snapshot, command: Command): Color =
     4.9    {
    4.10 -    val state = document.current_state(command)
    4.11 -    if (state.forks > 0) new Color(255, 228, 225)
    4.12 +    val state = snapshot.document.current_state(command)
    4.13 +    if (snapshot.is_outdated) new Color(240, 240, 240)
    4.14 +    else if (state.forks > 0) new Color(255, 228, 225)
    4.15      else if (state.forks < 0) Color.red
    4.16      else
    4.17        state.status match {
    4.18 @@ -105,9 +106,9 @@
    4.19          case Command_Set(changed) =>
    4.20            Swing_Thread.now {
    4.21              // FIXME cover doc states as well!!?
    4.22 -            val document = model.recent_document()
    4.23 -            if (changed.exists(document.commands(model.thy_name).contains))
    4.24 -              full_repaint(document, changed)
    4.25 +            val snapshot = model.snapshot()
    4.26 +            if (changed.exists(snapshot.node.commands.contains))
    4.27 +              full_repaint(snapshot, changed)
    4.28            }
    4.29  
    4.30          case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
    4.31 @@ -115,14 +116,16 @@
    4.32      }
    4.33    }
    4.34  
    4.35 -  def full_repaint(document: Document, changed: Set[Command])
    4.36 +  def full_repaint(snapshot: Change.Snapshot, changed: Set[Command])
    4.37    {
    4.38      Swing_Thread.assert()
    4.39  
    4.40 +    val document = snapshot.document
    4.41 +    val doc = snapshot.node
    4.42      val buffer = model.buffer
    4.43      var visible_change = false
    4.44  
    4.45 -    for ((command, start) <- document.command_starts(model.thy_name)) {
    4.46 +    for ((command, start) <- doc.command_starts) {
    4.47        if (changed(command)) {
    4.48          val stop = start + command.length
    4.49          val line1 = buffer.getLineOfOffset(model.to_current(document, start))
    4.50 @@ -148,18 +151,19 @@
    4.51        start: Array[Int], end: Array[Int], y0: Int, line_height: Int)
    4.52      {
    4.53        Swing_Thread.now {
    4.54 -        val document = model.recent_document()
    4.55 +        val snapshot = model.snapshot()
    4.56 +        val document = snapshot.document
    4.57 +        val doc = snapshot.node
    4.58          def from_current(pos: Int) = model.from_current(document, pos)
    4.59          def to_current(pos: Int) = model.to_current(document, pos)
    4.60  
    4.61          val command_range: Iterable[(Command, Int)] =
    4.62          {
    4.63 -          val range = document.command_range(model.thy_name, from_current(start(0)))
    4.64 +          val range = doc.command_range(from_current(start(0)))
    4.65            if (range.hasNext) {
    4.66              val (cmd0, start0) = range.next
    4.67              new Iterable[(Command, Int)] {
    4.68 -              def iterator =
    4.69 -                Document.command_starts(document.commands(model.thy_name).iterator(cmd0), start0)
    4.70 +              def iterator = Document.command_starts(doc.commands.iterator(cmd0), start0)
    4.71              }
    4.72            }
    4.73            else Iterable.empty
    4.74 @@ -183,7 +187,7 @@
    4.75                  val p = text_area.offsetToXY(line_start max to_current(command_start))
    4.76                  val q = text_area.offsetToXY(line_end min to_current(command_start + command.length))
    4.77                  assert(p.y == q.y)
    4.78 -                gfx.setColor(Document_View.choose_color(document, command))
    4.79 +                gfx.setColor(Document_View.choose_color(snapshot, command))
    4.80                  gfx.fillRect(p.x, y, q.x - p.x, line_height)
    4.81                }
    4.82              }
    4.83 @@ -196,9 +200,11 @@
    4.84  
    4.85      override def getToolTipText(x: Int, y: Int): String =
    4.86      {
    4.87 -      val document = model.recent_document()
    4.88 +      val snapshot = model.snapshot()
    4.89 +      val document = snapshot.document
    4.90 +      val doc = snapshot.node
    4.91        val offset = model.from_current(document, text_area.xyToOffset(x, y))
    4.92 -      document.command_at(model.thy_name, offset) match {
    4.93 +      doc.command_at(offset) match {
    4.94          case Some((command, command_start)) =>
    4.95            document.current_state(command).type_at(offset - command_start) match {
    4.96              case Some(text) => Isabelle.tooltip(text)
    4.97 @@ -213,7 +219,7 @@
    4.98    /* caret handling */
    4.99  
   4.100    def selected_command(): Option[Command] =
   4.101 -    model.recent_document().proper_command_at(model.thy_name, text_area.getCaretPosition)
   4.102 +    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
   4.103  
   4.104    private val caret_listener = new CaretListener {
   4.105      private val delay = Swing_Thread.delay_last(session.input_delay) {
   4.106 @@ -263,16 +269,16 @@
   4.107      {
   4.108        super.paintComponent(gfx)
   4.109        val buffer = model.buffer
   4.110 -      val document = model.recent_document()
   4.111 -      def to_current(pos: Int) = model.to_current(document, pos)
   4.112 +      val snapshot = model.snapshot()
   4.113 +      def to_current(pos: Int) = model.to_current(snapshot.document, pos)
   4.114        val saved_color = gfx.getColor  // FIXME needed!?
   4.115        try {
   4.116 -        for ((command, start) <- document.command_starts(model.thy_name) if !command.is_ignored) {
   4.117 +        for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
   4.118            val line1 = buffer.getLineOfOffset(to_current(start))
   4.119            val line2 = buffer.getLineOfOffset(to_current(start + command.length)) + 1
   4.120            val y = line_to_y(line1)
   4.121            val height = HEIGHT * (line2 - line1)
   4.122 -          gfx.setColor(Document_View.choose_color(document, command))
   4.123 +          gfx.setColor(Document_View.choose_color(snapshot, command))
   4.124            gfx.fillRect(0, y, getWidth - 1, height)
   4.125          }
   4.126        }

     5.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu Aug 05 14:35:35 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Thu Aug 05 16:58:18 2010 +0200
     5.3 @@ -42,9 +42,11 @@
     5.4    {
     5.5      Document_Model(buffer) match {
     5.6        case Some(model) =>
     5.7 -        val document = model.recent_document()
     5.8 +        val snapshot = model.snapshot()
     5.9 +        val document = snapshot.document
    5.10 +        val doc = snapshot.node
    5.11          val offset = model.from_current(document, original_offset)
    5.12 -        document.command_at(model.thy_name, offset) match {
    5.13 +        doc.command_at(offset) match {
    5.14            case Some((command, command_start)) =>
    5.15              document.current_state(command).ref_at(offset - command_start) match {
    5.16                case Some(ref) =>
    5.17 @@ -57,7 +59,7 @@
    5.18                    case Command.RefInfo(_, _, Some(id), Some(offset)) =>
    5.19                      Isabelle.session.lookup_entity(id) match {
    5.20                        case Some(ref_cmd: Command) =>
    5.21 -                        document.command_start(model.thy_name, ref_cmd) match {
    5.22 +                        doc.command_start(ref_cmd) match {
    5.23                            case Some(ref_cmd_start) =>
    5.24                              new Internal_Hyperlink(begin, end, line,
    5.25                                model.to_current(document, ref_cmd_start + offset - 1))

     6.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 05 14:35:35 2010 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Thu Aug 05 16:58:18 2010 +0200
     6.3 @@ -95,9 +95,9 @@
     6.4      import Isabelle_Sidekick.int_to_pos
     6.5  
     6.6      val root = data.root
     6.7 -    val document = model.recent_document()
     6.8 +    val doc = model.snapshot().node  // FIXME cover all nodes (!??)
     6.9      for {
    6.10 -      (command, command_start) <- document.command_range(model.thy_name, 0)
    6.11 +      (command, command_start) <- doc.command_range(0)
    6.12        if command.is_command && !stopped
    6.13      }
    6.14      {
    6.15 @@ -128,8 +128,10 @@
    6.16      import Isabelle_Sidekick.int_to_pos
    6.17  
    6.18      val root = data.root
    6.19 -    val document = model.recent_document()
    6.20 -    for ((command, command_start) <- document.command_range(model.thy_name, 0) if !stopped) {
    6.21 +    val snapshot = model.snapshot()
    6.22 +    val document = snapshot.document
    6.23 +    val doc = snapshot.node  // FIXME cover all nodes (!??)
    6.24 +    for ((command, command_start) <- doc.command_range(0) if !stopped) {
    6.25        root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
    6.26            {
    6.27              val content = command.source(node.start, node.stop).replace('\n', ' ')

     7.1 --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu Aug 05 14:35:35 2010 +0200
     7.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Thu Aug 05 16:58:18 2010 +0200
     7.3 @@ -151,7 +151,9 @@
     7.4      val start = model.buffer.getLineStartOffset(line)
     7.5      val stop = start + line_segment.count
     7.6  
     7.7 -    val document = model.recent_document()
     7.8 +    val snapshot = model.snapshot()
     7.9 +    val document = snapshot.document
    7.10 +    val doc = snapshot.node
    7.11      def to: Int => Int = model.to_current(document, _)
    7.12      def from: Int => Int = model.from_current(document, _)
    7.13  
    7.14 @@ -166,7 +168,7 @@
    7.15  
    7.16      var next_x = start
    7.17      for {
    7.18 -      (command, command_start) <- document.command_range(model.thy_name, from(start), from(stop))
    7.19 +      (command, command_start) <- doc.command_range(from(start), from(stop))
    7.20        markup <- document.current_state(command).highlight.flatten
    7.21        val abs_start = to(command_start + markup.start)
    7.22        val abs_stop = to(command_start + markup.stop)

     8.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu Aug 05 14:35:35 2010 +0200
     8.2 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu Aug 05 16:58:18 2010 +0200
     8.3 @@ -65,7 +65,7 @@
     8.4          case Some(doc_view) =>
     8.5            current_command match {
     8.6              case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
     8.7 -              val document = doc_view.model.recent_document
     8.8 +              val document = doc_view.model.snapshot().document
     8.9                val filtered_results =
    8.10                  document.current_state(cmd).results filter {
    8.11                    case XML.Elem(Markup.TRACING, _, _) => show_tracing