src/Pure/PIDE/document.scala
author wenzelm
Thu Aug 12 15:19:11 2010 +0200 (2010-08-12 ago)
changeset 38363 af7f41a8a0a8
parent 38361 b609d0b271fa
child 38364 827b90f18ff4
permissions -rw-r--r--
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
generic type Document.id (ML) / Document.ID;
wenzelm@36676
     1
/*  Title:      Pure/PIDE/document.scala
wenzelm@36676
     2
    Author:     Makarius
wenzelm@36676
     3
wenzelm@38150
     4
Document as collection of named nodes, each consisting of an editable
wenzelm@38150
     5
list of commands.
wenzelm@36676
     6
*/
wenzelm@34407
     7
wenzelm@34871
     8
package isabelle
wenzelm@34318
     9
wenzelm@34760
    10
wenzelm@38150
    11
import scala.collection.mutable
wenzelm@37073
    12
import scala.annotation.tailrec
wenzelm@37073
    13
wenzelm@37073
    14
wenzelm@34823
    15
object Document
wenzelm@34483
    16
{
wenzelm@38227
    17
  /* formal identifiers */
wenzelm@38150
    18
wenzelm@38363
    19
  type ID = Long
wenzelm@38363
    20
  type Exec_ID = ID
wenzelm@38363
    21
  type Command_ID = ID
wenzelm@38363
    22
  type Version_ID = ID
wenzelm@38150
    23
wenzelm@38363
    24
  val NO_ID: ID = 0
wenzelm@38355
    25
wenzelm@38363
    26
  def parse_id(s: String): ID = java.lang.Long.parseLong(s)
wenzelm@38363
    27
  def print_id(id: ID): String = id.toString
wenzelm@38150
    28
wenzelm@38150
    29
wenzelm@34818
    30
wenzelm@38227
    31
  /** named document nodes **/
wenzelm@38151
    32
wenzelm@38151
    33
  object Node
wenzelm@38151
    34
  {
wenzelm@38151
    35
    val empty: Node = new Node(Linear_Set())
wenzelm@38227
    36
wenzelm@38227
    37
    def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
wenzelm@38227
    38
    {
wenzelm@38227
    39
      var i = offset
wenzelm@38227
    40
      for (command <- commands) yield {
wenzelm@38227
    41
        val start = i
wenzelm@38227
    42
        i += command.length
wenzelm@38227
    43
        (command, start)
wenzelm@38227
    44
      }
wenzelm@38227
    45
    }
wenzelm@38151
    46
  }
wenzelm@38151
    47
wenzelm@38151
    48
  class Node(val commands: Linear_Set[Command])
wenzelm@38151
    49
  {
wenzelm@38151
    50
    /* command ranges */
wenzelm@38151
    51
wenzelm@38151
    52
    def command_starts: Iterator[(Command, Int)] =
wenzelm@38227
    53
      Node.command_starts(commands.iterator)
wenzelm@38151
    54
wenzelm@38151
    55
    def command_start(cmd: Command): Option[Int] =
wenzelm@38151
    56
      command_starts.find(_._1 == cmd).map(_._2)
wenzelm@38151
    57
wenzelm@38151
    58
    def command_range(i: Int): Iterator[(Command, Int)] =
wenzelm@38151
    59
      command_starts dropWhile { case (cmd, start) => start + cmd.length <= i }
wenzelm@38151
    60
wenzelm@38151
    61
    def command_range(i: Int, j: Int): Iterator[(Command, Int)] =
wenzelm@38151
    62
      command_range(i) takeWhile { case (_, start) => start < j }
wenzelm@38151
    63
wenzelm@38151
    64
    def command_at(i: Int): Option[(Command, Int)] =
wenzelm@38151
    65
    {
wenzelm@38151
    66
      val range = command_range(i)
wenzelm@38151
    67
      if (range.hasNext) Some(range.next) else None
wenzelm@38151
    68
    }
wenzelm@38151
    69
wenzelm@38151
    70
    def proper_command_at(i: Int): Option[Command] =
wenzelm@38151
    71
      command_at(i) match {
wenzelm@38151
    72
        case Some((command, _)) =>
wenzelm@38151
    73
          commands.reverse_iterator(command).find(cmd => !cmd.is_ignored)
wenzelm@38151
    74
        case None => None
wenzelm@38151
    75
      }
wenzelm@38151
    76
  }
wenzelm@38151
    77
wenzelm@38151
    78
wenzelm@38150
    79
  /* initial document */
wenzelm@34485
    80
wenzelm@38150
    81
  val init: Document =
wenzelm@34835
    82
  {
wenzelm@38151
    83
    val doc = new Document(NO_ID, Map().withDefaultValue(Node.empty), Map())
wenzelm@38363
    84
    doc.assign_execs(Nil)
wenzelm@34835
    85
    doc
wenzelm@34835
    86
  }
immler@34660
    87
wenzelm@34859
    88
wenzelm@34859
    89
wenzelm@38227
    90
  /** changes of plain text, eventually resulting in document edits **/
wenzelm@38151
    91
wenzelm@38151
    92
  type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
wenzelm@38151
    93
wenzelm@38151
    94
  type Edit[C] =
wenzelm@38151
    95
   (String,  // node name
wenzelm@38151
    96
    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
wenzelm@34859
    97
wenzelm@38227
    98
  abstract class Snapshot
wenzelm@38227
    99
  {
wenzelm@38227
   100
    val document: Document
wenzelm@38227
   101
    val node: Document.Node
wenzelm@38227
   102
    val is_outdated: Boolean
wenzelm@38227
   103
    def convert(offset: Int): Int
wenzelm@38227
   104
    def revert(offset: Int): Int
wenzelm@38361
   105
    def state(command: Command): Command.State
wenzelm@38227
   106
  }
wenzelm@38227
   107
wenzelm@38227
   108
  object Change
wenzelm@38227
   109
  {
wenzelm@38227
   110
    val init = new Change(NO_ID, None, Nil, Future.value(Nil, Document.init))
wenzelm@38227
   111
  }
wenzelm@38227
   112
wenzelm@38227
   113
  class Change(
wenzelm@38227
   114
    val id: Version_ID,
wenzelm@38227
   115
    val parent: Option[Change],
wenzelm@38227
   116
    val edits: List[Node_Text_Edit],
wenzelm@38227
   117
    val result: Future[(List[Edit[Command]], Document)])
wenzelm@38227
   118
  {
wenzelm@38227
   119
    def ancestors: Iterator[Change] = new Iterator[Change]
wenzelm@38227
   120
    {
wenzelm@38227
   121
      private var state: Option[Change] = Some(Change.this)
wenzelm@38227
   122
      def hasNext = state.isDefined
wenzelm@38227
   123
      def next =
wenzelm@38227
   124
        state match {
wenzelm@38227
   125
          case Some(change) => state = change.parent; change
wenzelm@38227
   126
          case None => throw new NoSuchElementException("next on empty iterator")
wenzelm@38227
   127
        }
wenzelm@38227
   128
    }
wenzelm@38227
   129
wenzelm@38227
   130
    def join_document: Document = result.join._2
wenzelm@38227
   131
    def is_assigned: Boolean = result.is_finished && join_document.assignment.is_finished
wenzelm@38227
   132
wenzelm@38227
   133
    def snapshot(name: String, pending_edits: List[Text_Edit]): Snapshot =
wenzelm@38227
   134
    {
wenzelm@38227
   135
      val latest = Change.this
wenzelm@38227
   136
      val stable = latest.ancestors.find(_.is_assigned)
wenzelm@38227
   137
      require(stable.isDefined)
wenzelm@38227
   138
wenzelm@38227
   139
      val edits =
wenzelm@38227
   140
        (pending_edits /: latest.ancestors.takeWhile(_ != stable.get))((edits, change) =>
wenzelm@38227
   141
            (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
wenzelm@38227
   142
      lazy val reverse_edits = edits.reverse
wenzelm@38227
   143
wenzelm@38227
   144
      new Snapshot {
wenzelm@38227
   145
        val document = stable.get.join_document
wenzelm@38227
   146
        val node = document.nodes(name)
wenzelm@38227
   147
        val is_outdated = !(pending_edits.isEmpty && latest == stable.get)
wenzelm@38227
   148
        def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
wenzelm@38227
   149
        def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
wenzelm@38361
   150
        def state(command: Command): Command.State = document.current_state(command)
wenzelm@38227
   151
      }
wenzelm@38227
   152
    }
wenzelm@38227
   153
  }
wenzelm@38227
   154
wenzelm@38227
   155
wenzelm@38227
   156
wenzelm@38227
   157
  /** editing **/
wenzelm@38227
   158
wenzelm@38150
   159
  def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
wenzelm@38151
   160
      edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
wenzelm@34824
   161
  {
wenzelm@34840
   162
    require(old_doc.assignment.is_finished)
wenzelm@34840
   163
wenzelm@34859
   164
wenzelm@34859
   165
    /* unparsed dummy commands */
immler@34538
   166
wenzelm@34859
   167
    def unparsed(source: String) =
wenzelm@38220
   168
      new Command(NO_ID, List(Token(Token.Kind.UNPARSED, source)))
wenzelm@34859
   169
wenzelm@38220
   170
    def is_unparsed(command: Command) = command.id == NO_ID
wenzelm@34835
   171
wenzelm@34859
   172
wenzelm@34859
   173
    /* phase 1: edit individual command source */
wenzelm@34859
   174
wenzelm@38150
   175
    @tailrec def edit_text(eds: List[Text_Edit],
wenzelm@38150
   176
        commands: Linear_Set[Command]): Linear_Set[Command] =
wenzelm@34859
   177
    {
wenzelm@34859
   178
      eds match {
wenzelm@34859
   179
        case e :: es =>
wenzelm@38227
   180
          Node.command_starts(commands.iterator).find {
wenzelm@34866
   181
            case (cmd, cmd_start) =>
wenzelm@37685
   182
              e.can_edit(cmd.source, cmd_start) ||
wenzelm@37685
   183
                e.is_insert && e.start == cmd_start + cmd.length
wenzelm@34863
   184
          } match {
wenzelm@34866
   185
            case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
wenzelm@34866
   186
              val (rest, text) = e.edit(cmd.source, cmd_start)
wenzelm@34866
   187
              val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
wenzelm@34863
   188
              edit_text(rest.toList ::: es, new_commands)
wenzelm@34318
   189
wenzelm@34866
   190
            case Some((cmd, cmd_start)) =>
wenzelm@34866
   191
              edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
wenzelm@34866
   192
wenzelm@34859
   193
            case None =>
wenzelm@34866
   194
              require(e.is_insert && e.start == 0)
wenzelm@34863
   195
              edit_text(es, commands.insert_after(None, unparsed(e.text)))
wenzelm@34859
   196
          }
wenzelm@34863
   197
        case Nil => commands
wenzelm@34318
   198
      }
wenzelm@34318
   199
    }
wenzelm@34582
   200
wenzelm@34818
   201
wenzelm@34866
   202
    /* phase 2: recover command spans */
wenzelm@34859
   203
wenzelm@37073
   204
    @tailrec def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
wenzelm@34859
   205
    {
wenzelm@36011
   206
      commands.iterator.find(is_unparsed) match {
wenzelm@34859
   207
        case Some(first_unparsed) =>
wenzelm@37071
   208
          val first =
wenzelm@37072
   209
            commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
wenzelm@37071
   210
          val last =
wenzelm@37071
   211
            commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
wenzelm@37071
   212
          val range =
wenzelm@37071
   213
            commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
wenzelm@34859
   214
wenzelm@37071
   215
          val sources = range.flatMap(_.span.map(_.source))
wenzelm@34866
   216
          val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
wenzelm@34485
   217
wenzelm@34859
   218
          val (before_edit, spans1) =
wenzelm@37071
   219
            if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
wenzelm@37071
   220
              (Some(first), spans0.tail)
wenzelm@37071
   221
            else (commands.prev(first), spans0)
immler@34544
   222
wenzelm@34859
   223
          val (after_edit, spans2) =
wenzelm@37071
   224
            if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
wenzelm@37071
   225
              (Some(last), spans1.take(spans1.length - 1))
wenzelm@37071
   226
            else (commands.next(last), spans1)
wenzelm@34859
   227
wenzelm@34863
   228
          val inserted = spans2.map(span => new Command(session.create_id(), span))
wenzelm@34863
   229
          val new_commands =
wenzelm@34863
   230
            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
wenzelm@34866
   231
          parse_spans(new_commands)
wenzelm@34485
   232
wenzelm@34863
   233
        case None => commands
wenzelm@34485
   234
      }
wenzelm@34485
   235
    }
wenzelm@34739
   236
immler@34554
   237
wenzelm@34859
   238
    /* phase 3: resulting document edits */
wenzelm@34859
   239
wenzelm@38150
   240
    {
wenzelm@38150
   241
      val doc_edits = new mutable.ListBuffer[Edit[Command]]
wenzelm@38150
   242
      var nodes = old_doc.nodes
wenzelm@38363
   243
      var former_assignment = old_doc.assignment.join
immler@34660
   244
wenzelm@38150
   245
      for ((name, text_edits) <- edits) {
wenzelm@38151
   246
        val commands0 = nodes(name).commands
wenzelm@38150
   247
        val commands1 = edit_text(text_edits, commands0)
wenzelm@38220
   248
        val commands2 = parse_spans(commands1)   // FIXME somewhat slow
wenzelm@34863
   249
wenzelm@38150
   250
        val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
wenzelm@38150
   251
        val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
wenzelm@38150
   252
wenzelm@38150
   253
        val cmd_edits =
wenzelm@38150
   254
          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
wenzelm@38150
   255
          inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
immler@34660
   256
wenzelm@38150
   257
        doc_edits += (name -> Some(cmd_edits))
wenzelm@38151
   258
        nodes += (name -> new Node(commands2))
wenzelm@38363
   259
        former_assignment --= removed_commands
wenzelm@38150
   260
      }
wenzelm@38363
   261
      (doc_edits.toList, new Document(new_id, nodes, former_assignment))
wenzelm@38150
   262
    }
wenzelm@34485
   263
  }
wenzelm@34840
   264
}
wenzelm@34840
   265
wenzelm@34855
   266
wenzelm@34840
   267
class Document(
wenzelm@38150
   268
    val id: Document.Version_ID,
wenzelm@38151
   269
    val nodes: Map[String, Document.Node],
wenzelm@38363
   270
    former_assignment: Map[Command, Command])  // FIXME !?
wenzelm@34840
   271
{
wenzelm@34855
   272
  /* command state assignment */
wenzelm@34840
   273
wenzelm@34840
   274
  val assignment = Future.promise[Map[Command, Command]]
wenzelm@34853
   275
  def await_assignment { assignment.join }
wenzelm@34840
   276
wenzelm@38363
   277
  @volatile private var tmp_assignment = former_assignment
wenzelm@34840
   278
wenzelm@38363
   279
  def assign_execs(execs: List[(Command, Command)])
wenzelm@34840
   280
  {
wenzelm@38363
   281
    assignment.fulfill(tmp_assignment ++ execs)
wenzelm@38363
   282
    tmp_assignment = Map()
wenzelm@34840
   283
  }
wenzelm@34840
   284
wenzelm@38361
   285
  def current_state(cmd: Command): Command.State =
wenzelm@34840
   286
  {
wenzelm@34840
   287
    require(assignment.is_finished)
wenzelm@36990
   288
    (assignment.join).get(cmd) match {
wenzelm@36990
   289
      case Some(cmd_state) => cmd_state.current_state
wenzelm@38361
   290
      case None => new Command.State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup)
wenzelm@36990
   291
    }
wenzelm@34840
   292
  }
wenzelm@34318
   293
}