src/Pure/PIDE/document.scala
author wenzelm
Sat Aug 14 11:52:24 2010 +0200 (2010-08-14 ago)
changeset 38373 e8197eea3cd0
parent 38370 8b15d0f98962
child 38374 7eb0f6991e25
permissions -rw-r--r--
tuned;
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@38373
    20
  type Version_ID = ID
wenzelm@38363
    21
  type Command_ID = ID
wenzelm@38373
    22
  type Exec_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@38370
    81
  val init: Document = new Document(NO_ID, Map().withDefaultValue(Node.empty))
immler@34660
    82
wenzelm@34859
    83
wenzelm@34859
    84
wenzelm@38227
    85
  /** changes of plain text, eventually resulting in document edits **/
wenzelm@38151
    86
wenzelm@38151
    87
  type Node_Text_Edit = (String, List[Text_Edit])  // FIXME None: remove
wenzelm@38151
    88
wenzelm@38151
    89
  type Edit[C] =
wenzelm@38151
    90
   (String,  // node name
wenzelm@38151
    91
    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
wenzelm@34859
    92
wenzelm@38227
    93
  abstract class Snapshot
wenzelm@38227
    94
  {
wenzelm@38227
    95
    val document: Document
wenzelm@38227
    96
    val node: Document.Node
wenzelm@38227
    97
    val is_outdated: Boolean
wenzelm@38227
    98
    def convert(offset: Int): Int
wenzelm@38227
    99
    def revert(offset: Int): Int
wenzelm@38370
   100
    def lookup_command(id: Command_ID): Option[Command]
wenzelm@38361
   101
    def state(command: Command): Command.State
wenzelm@38227
   102
  }
wenzelm@38227
   103
wenzelm@38227
   104
  object Change
wenzelm@38227
   105
  {
wenzelm@38366
   106
    val init = new Change(Future.value(Document.init), Nil, Future.value(Nil, Document.init))
wenzelm@38227
   107
  }
wenzelm@38227
   108
wenzelm@38227
   109
  class Change(
wenzelm@38366
   110
    val prev: Future[Document],
wenzelm@38227
   111
    val edits: List[Node_Text_Edit],
wenzelm@38227
   112
    val result: Future[(List[Edit[Command]], Document)])
wenzelm@38227
   113
  {
wenzelm@38366
   114
    val document: Future[Document] = result.map(_._2)
wenzelm@38366
   115
    def is_finished: Boolean = prev.is_finished && document.is_finished
wenzelm@38227
   116
  }
wenzelm@38227
   117
wenzelm@38227
   118
wenzelm@38227
   119
wenzelm@38227
   120
  /** editing **/
wenzelm@38227
   121
wenzelm@38364
   122
  def text_edits(session: Session, old_doc: Document, edits: List[Node_Text_Edit])
wenzelm@38364
   123
      : (List[Edit[Command]], Document) =
wenzelm@34824
   124
  {
wenzelm@34859
   125
    /* phase 1: edit individual command source */
wenzelm@34859
   126
wenzelm@38150
   127
    @tailrec def edit_text(eds: List[Text_Edit],
wenzelm@38150
   128
        commands: Linear_Set[Command]): Linear_Set[Command] =
wenzelm@34859
   129
    {
wenzelm@34859
   130
      eds match {
wenzelm@34859
   131
        case e :: es =>
wenzelm@38227
   132
          Node.command_starts(commands.iterator).find {
wenzelm@34866
   133
            case (cmd, cmd_start) =>
wenzelm@37685
   134
              e.can_edit(cmd.source, cmd_start) ||
wenzelm@37685
   135
                e.is_insert && e.start == cmd_start + cmd.length
wenzelm@34863
   136
          } match {
wenzelm@34866
   137
            case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
wenzelm@34866
   138
              val (rest, text) = e.edit(cmd.source, cmd_start)
wenzelm@38367
   139
              val new_commands = commands.insert_after(Some(cmd), Command.unparsed(text)) - cmd
wenzelm@34863
   140
              edit_text(rest.toList ::: es, new_commands)
wenzelm@34318
   141
wenzelm@34866
   142
            case Some((cmd, cmd_start)) =>
wenzelm@38367
   143
              edit_text(es, commands.insert_after(Some(cmd), Command.unparsed(e.text)))
wenzelm@34866
   144
wenzelm@34859
   145
            case None =>
wenzelm@34866
   146
              require(e.is_insert && e.start == 0)
wenzelm@38367
   147
              edit_text(es, commands.insert_after(None, Command.unparsed(e.text)))
wenzelm@34859
   148
          }
wenzelm@34863
   149
        case Nil => commands
wenzelm@34318
   150
      }
wenzelm@34318
   151
    }
wenzelm@34582
   152
wenzelm@34818
   153
wenzelm@34866
   154
    /* phase 2: recover command spans */
wenzelm@34859
   155
wenzelm@37073
   156
    @tailrec def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
wenzelm@34859
   157
    {
wenzelm@38367
   158
      commands.iterator.find(_.is_unparsed) match {
wenzelm@34859
   159
        case Some(first_unparsed) =>
wenzelm@37071
   160
          val first =
wenzelm@37072
   161
            commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
wenzelm@37071
   162
          val last =
wenzelm@37071
   163
            commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
wenzelm@37071
   164
          val range =
wenzelm@37071
   165
            commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
wenzelm@34859
   166
wenzelm@37071
   167
          val sources = range.flatMap(_.span.map(_.source))
wenzelm@34866
   168
          val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
wenzelm@34485
   169
wenzelm@34859
   170
          val (before_edit, spans1) =
wenzelm@37071
   171
            if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
wenzelm@37071
   172
              (Some(first), spans0.tail)
wenzelm@37071
   173
            else (commands.prev(first), spans0)
immler@34544
   174
wenzelm@34859
   175
          val (after_edit, spans2) =
wenzelm@37071
   176
            if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
wenzelm@37071
   177
              (Some(last), spans1.take(spans1.length - 1))
wenzelm@37071
   178
            else (commands.next(last), spans1)
wenzelm@34859
   179
wenzelm@34863
   180
          val inserted = spans2.map(span => new Command(session.create_id(), span))
wenzelm@34863
   181
          val new_commands =
wenzelm@34863
   182
            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
wenzelm@34866
   183
          parse_spans(new_commands)
wenzelm@34485
   184
wenzelm@34863
   185
        case None => commands
wenzelm@34485
   186
      }
wenzelm@34485
   187
    }
wenzelm@34739
   188
immler@34554
   189
wenzelm@38373
   190
    /* resulting document edits */
wenzelm@34859
   191
wenzelm@38150
   192
    {
wenzelm@38150
   193
      val doc_edits = new mutable.ListBuffer[Edit[Command]]
wenzelm@38150
   194
      var nodes = old_doc.nodes
immler@34660
   195
wenzelm@38150
   196
      for ((name, text_edits) <- edits) {
wenzelm@38151
   197
        val commands0 = nodes(name).commands
wenzelm@38150
   198
        val commands1 = edit_text(text_edits, commands0)
wenzelm@38220
   199
        val commands2 = parse_spans(commands1)   // FIXME somewhat slow
wenzelm@34863
   200
wenzelm@38150
   201
        val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
wenzelm@38150
   202
        val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
wenzelm@38150
   203
wenzelm@38150
   204
        val cmd_edits =
wenzelm@38150
   205
          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
wenzelm@38150
   206
          inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
immler@34660
   207
wenzelm@38150
   208
        doc_edits += (name -> Some(cmd_edits))
wenzelm@38151
   209
        nodes += (name -> new Node(commands2))
wenzelm@38370
   210
      }
wenzelm@38370
   211
      (doc_edits.toList, new Document(session.create_id(), nodes))
wenzelm@38370
   212
    }
wenzelm@38370
   213
  }
wenzelm@38370
   214
wenzelm@38370
   215
wenzelm@38370
   216
wenzelm@38370
   217
  /** global state -- accumulated prover results **/
wenzelm@38370
   218
wenzelm@38370
   219
  object State
wenzelm@38370
   220
  {
wenzelm@38373
   221
    class Fail(state: State) extends Exception
wenzelm@38373
   222
wenzelm@38370
   223
    val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil)
wenzelm@38370
   224
wenzelm@38370
   225
    class Assignment(former_assignment: Map[Command, Exec_ID])
wenzelm@38370
   226
    {
wenzelm@38370
   227
      @volatile private var tmp_assignment = former_assignment
wenzelm@38370
   228
      private val promise = Future.promise[Map[Command, Exec_ID]]
wenzelm@38370
   229
      def is_finished: Boolean = promise.is_finished
wenzelm@38370
   230
      def join: Map[Command, Exec_ID] = promise.join
wenzelm@38370
   231
      def assign(command_execs: List[(Command, Exec_ID)])
wenzelm@38370
   232
      {
wenzelm@38370
   233
        promise.fulfill(tmp_assignment ++ command_execs)
wenzelm@38370
   234
        tmp_assignment = Map()
wenzelm@38150
   235
      }
wenzelm@38370
   236
    }
wenzelm@38370
   237
  }
wenzelm@38370
   238
wenzelm@38370
   239
  case class State(
wenzelm@38373
   240
    val documents: Map[Version_ID, Document] = Map(),
wenzelm@38370
   241
    val commands: Map[Command_ID, Command.State] = Map(),
wenzelm@38370
   242
    val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(),
wenzelm@38370
   243
    val assignments: Map[Document, State.Assignment] = Map(),
wenzelm@38370
   244
    val disposed: Set[ID] = Set())  // FIXME unused!?
wenzelm@38370
   245
  {
wenzelm@38373
   246
    private def fail[A]: A = throw new State.Fail(this)
wenzelm@38370
   247
wenzelm@38370
   248
    def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State =
wenzelm@38370
   249
    {
wenzelm@38370
   250
      val id = document.id
wenzelm@38370
   251
      if (documents.isDefinedAt(id) || disposed(id)) fail
wenzelm@38370
   252
      copy(documents = documents + (id -> document),
wenzelm@38370
   253
        assignments = assignments + (document -> new State.Assignment(former_assignment)))
wenzelm@38370
   254
    }
wenzelm@38370
   255
wenzelm@38373
   256
    def define_command(command: Command): State =
wenzelm@38373
   257
    {
wenzelm@38373
   258
      val id = command.id
wenzelm@38373
   259
      if (commands.isDefinedAt(id) || disposed(id)) fail
wenzelm@38373
   260
      copy(commands = commands + (id -> command.empty_state))
wenzelm@38373
   261
    }
wenzelm@38373
   262
wenzelm@38370
   263
    def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
wenzelm@38373
   264
wenzelm@38373
   265
    def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
wenzelm@38370
   266
    def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
wenzelm@38370
   267
    def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
wenzelm@38370
   268
    def the_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail)
wenzelm@38370
   269
wenzelm@38370
   270
    def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
wenzelm@38370
   271
      execs.get(id) match {
wenzelm@38370
   272
        case Some((st, docs)) =>
wenzelm@38370
   273
          val new_st = st.accumulate(message)
wenzelm@38370
   274
          (new_st, copy(execs = execs + (id -> (new_st, docs))))
wenzelm@38370
   275
        case None =>
wenzelm@38370
   276
          commands.get(id) match {
wenzelm@38370
   277
            case Some(st) =>
wenzelm@38370
   278
              val new_st = st.accumulate(message)
wenzelm@38370
   279
              (new_st, copy(commands = commands + (id -> new_st)))
wenzelm@38370
   280
            case None => fail
wenzelm@38370
   281
          }
wenzelm@38370
   282
      }
wenzelm@38370
   283
wenzelm@38370
   284
    def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
wenzelm@38370
   285
    {
wenzelm@38370
   286
      val doc = the_document(id)
wenzelm@38370
   287
      val docs = Set(doc)  // FIXME unused (!?)
wenzelm@38370
   288
wenzelm@38370
   289
      var new_execs = execs
wenzelm@38370
   290
      val assigned_execs =
wenzelm@38370
   291
        for ((cmd_id, exec_id) <- edits) yield {
wenzelm@38370
   292
          val st = the_command(cmd_id)
wenzelm@38370
   293
          if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
wenzelm@38370
   294
          new_execs += (exec_id -> (st, docs))
wenzelm@38370
   295
          (st.command, exec_id)
wenzelm@38370
   296
        }
wenzelm@38370
   297
      the_assignment(doc).assign(assigned_execs)  // FIXME explicit value instead of promise (!?)
wenzelm@38370
   298
      copy(execs = new_execs)
wenzelm@38370
   299
    }
wenzelm@38370
   300
wenzelm@38370
   301
    def is_assigned(document: Document): Boolean =
wenzelm@38370
   302
      assignments.get(document) match {
wenzelm@38370
   303
        case Some(assgn) => assgn.is_finished
wenzelm@38370
   304
        case None => false
wenzelm@38370
   305
      }
wenzelm@38370
   306
wenzelm@38370
   307
    def command_state(document: Document, command: Command): Command.State =
wenzelm@38370
   308
    {
wenzelm@38370
   309
      val assgn = the_assignment(document)
wenzelm@38370
   310
      require(assgn.is_finished)
wenzelm@38370
   311
      the_exec_state(assgn.join.getOrElse(command, fail))
wenzelm@38150
   312
    }
wenzelm@34485
   313
  }
wenzelm@34840
   314
}
wenzelm@34840
   315
wenzelm@34855
   316
wenzelm@34840
   317
class Document(
wenzelm@38150
   318
    val id: Document.Version_ID,
wenzelm@38370
   319
    val nodes: Map[String, Document.Node])
wenzelm@34840
   320