src/Pure/PIDE/document.scala
author wenzelm
Thu Aug 05 14:35:35 2010 +0200 (2010-08-05)
changeset 38150 67fc24df3721
parent 37849 4f9de312cc23
child 38151 2837c952ca31
permissions -rw-r--r--
simplified/refined document model: collection of named nodes, without proper dependencies yet;
moved basic type definitions for ids and edits from Isar_Document to Document;
removed begin_document/end_document for now -- nodes emerge via edits;
edits refer to named nodes explicitly;
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@38150
    17
  /* unique identifiers */
wenzelm@38150
    18
wenzelm@38150
    19
  type State_ID = String
wenzelm@38150
    20
  type Command_ID = String
wenzelm@38150
    21
  type Version_ID = String
wenzelm@38150
    22
wenzelm@38150
    23
  val NO_ID = ""
wenzelm@38150
    24
wenzelm@38150
    25
wenzelm@38150
    26
  /* nodes */
wenzelm@38150
    27
wenzelm@38150
    28
  object Node { type Text_Edit = (String, List[isabelle.Text_Edit]) }  // FIXME None: remove
wenzelm@38150
    29
wenzelm@38150
    30
  type Edit[C] =
wenzelm@38150
    31
   (String,  // node name
wenzelm@38150
    32
    Option[List[(Option[C], Option[C])]])  // None: remove, Some: insert/remove commands
wenzelm@38150
    33
wenzelm@38150
    34
wenzelm@34859
    35
  /* command start positions */
wenzelm@34818
    36
wenzelm@37685
    37
  def command_starts(commands: Iterator[Command], offset: Int = 0): Iterator[(Command, Int)] =
wenzelm@34859
    38
  {
wenzelm@37685
    39
    var i = offset
wenzelm@37685
    40
    for (command <- commands) yield {
wenzelm@37685
    41
      val start = i
wenzelm@37685
    42
      i += command.length
wenzelm@37685
    43
      (command, start)
wenzelm@34859
    44
    }
wenzelm@34859
    45
  }
wenzelm@34859
    46
wenzelm@34859
    47
wenzelm@38150
    48
  /* initial document */
wenzelm@34485
    49
wenzelm@38150
    50
  val init: Document =
wenzelm@34835
    51
  {
wenzelm@38150
    52
    val doc = new Document(NO_ID, Map().withDefaultValue(Linear_Set()), Map())
wenzelm@34835
    53
    doc.assign_states(Nil)
wenzelm@34835
    54
    doc
wenzelm@34835
    55
  }
immler@34660
    56
wenzelm@34859
    57
wenzelm@34859
    58
wenzelm@34859
    59
  /** document edits **/
wenzelm@34859
    60
wenzelm@38150
    61
  def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
wenzelm@38150
    62
      edits: List[Node.Text_Edit]): (List[Edit[Command]], Document) =
wenzelm@34824
    63
  {
wenzelm@34840
    64
    require(old_doc.assignment.is_finished)
wenzelm@34840
    65
wenzelm@34859
    66
wenzelm@34859
    67
    /* unparsed dummy commands */
immler@34538
    68
wenzelm@34859
    69
    def unparsed(source: String) =
wenzelm@36956
    70
      new Command(null, List(Token(Token.Kind.UNPARSED, source)))
wenzelm@34859
    71
wenzelm@34860
    72
    def is_unparsed(command: Command) = command.id == null
wenzelm@34835
    73
wenzelm@34859
    74
wenzelm@34859
    75
    /* phase 1: edit individual command source */
wenzelm@34859
    76
wenzelm@38150
    77
    @tailrec def edit_text(eds: List[Text_Edit],
wenzelm@38150
    78
        commands: Linear_Set[Command]): Linear_Set[Command] =
wenzelm@34859
    79
    {
wenzelm@34859
    80
      eds match {
wenzelm@34859
    81
        case e :: es =>
wenzelm@37685
    82
          command_starts(commands.iterator).find {
wenzelm@34866
    83
            case (cmd, cmd_start) =>
wenzelm@37685
    84
              e.can_edit(cmd.source, cmd_start) ||
wenzelm@37685
    85
                e.is_insert && e.start == cmd_start + cmd.length
wenzelm@34863
    86
          } match {
wenzelm@34866
    87
            case Some((cmd, cmd_start)) if e.can_edit(cmd.source, cmd_start) =>
wenzelm@34866
    88
              val (rest, text) = e.edit(cmd.source, cmd_start)
wenzelm@34866
    89
              val new_commands = commands.insert_after(Some(cmd), unparsed(text)) - cmd
wenzelm@34863
    90
              edit_text(rest.toList ::: es, new_commands)
wenzelm@34318
    91
wenzelm@34866
    92
            case Some((cmd, cmd_start)) =>
wenzelm@34866
    93
              edit_text(es, commands.insert_after(Some(cmd), unparsed(e.text)))
wenzelm@34866
    94
wenzelm@34859
    95
            case None =>
wenzelm@34866
    96
              require(e.is_insert && e.start == 0)
wenzelm@34863
    97
              edit_text(es, commands.insert_after(None, unparsed(e.text)))
wenzelm@34859
    98
          }
wenzelm@34863
    99
        case Nil => commands
wenzelm@34318
   100
      }
wenzelm@34318
   101
    }
wenzelm@34582
   102
wenzelm@34818
   103
wenzelm@34866
   104
    /* phase 2: recover command spans */
wenzelm@34859
   105
wenzelm@37073
   106
    @tailrec def parse_spans(commands: Linear_Set[Command]): Linear_Set[Command] =
wenzelm@34859
   107
    {
wenzelm@36011
   108
      commands.iterator.find(is_unparsed) match {
wenzelm@34859
   109
        case Some(first_unparsed) =>
wenzelm@37071
   110
          val first =
wenzelm@37072
   111
            commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
wenzelm@37071
   112
          val last =
wenzelm@37071
   113
            commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
wenzelm@37071
   114
          val range =
wenzelm@37071
   115
            commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
wenzelm@34859
   116
wenzelm@37071
   117
          val sources = range.flatMap(_.span.map(_.source))
wenzelm@34866
   118
          val spans0 = Thy_Syntax.parse_spans(session.current_syntax.scan(sources.mkString))
wenzelm@34485
   119
wenzelm@34859
   120
          val (before_edit, spans1) =
wenzelm@37071
   121
            if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
wenzelm@37071
   122
              (Some(first), spans0.tail)
wenzelm@37071
   123
            else (commands.prev(first), spans0)
immler@34544
   124
wenzelm@34859
   125
          val (after_edit, spans2) =
wenzelm@37071
   126
            if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
wenzelm@37071
   127
              (Some(last), spans1.take(spans1.length - 1))
wenzelm@37071
   128
            else (commands.next(last), spans1)
wenzelm@34859
   129
wenzelm@34863
   130
          val inserted = spans2.map(span => new Command(session.create_id(), span))
wenzelm@34863
   131
          val new_commands =
wenzelm@34863
   132
            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
wenzelm@34866
   133
          parse_spans(new_commands)
wenzelm@34485
   134
wenzelm@34863
   135
        case None => commands
wenzelm@34485
   136
      }
wenzelm@34485
   137
    }
wenzelm@34739
   138
immler@34554
   139
wenzelm@34859
   140
    /* phase 3: resulting document edits */
wenzelm@34859
   141
wenzelm@38150
   142
    {
wenzelm@38150
   143
      val doc_edits = new mutable.ListBuffer[Edit[Command]]
wenzelm@38150
   144
      var nodes = old_doc.nodes
wenzelm@38150
   145
      var former_states = old_doc.assignment.join
immler@34660
   146
wenzelm@38150
   147
      for ((name, text_edits) <- edits) {
wenzelm@38150
   148
        val commands0 = nodes(name)
wenzelm@38150
   149
        val commands1 = edit_text(text_edits, commands0)
wenzelm@38150
   150
        val commands2 = parse_spans(commands1)
wenzelm@34863
   151
wenzelm@38150
   152
        val removed_commands = commands0.iterator.filter(!commands2.contains(_)).toList
wenzelm@38150
   153
        val inserted_commands = commands2.iterator.filter(!commands0.contains(_)).toList
wenzelm@38150
   154
wenzelm@38150
   155
        val cmd_edits =
wenzelm@38150
   156
          removed_commands.reverse.map(cmd => (commands0.prev(cmd), None)) :::
wenzelm@38150
   157
          inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
immler@34660
   158
wenzelm@38150
   159
        doc_edits += (name -> Some(cmd_edits))
wenzelm@38150
   160
        nodes += (name -> commands2)
wenzelm@38150
   161
        former_states --= removed_commands
wenzelm@38150
   162
      }
wenzelm@38150
   163
      (doc_edits.toList, new Document(new_id, nodes, former_states))
wenzelm@38150
   164
    }
wenzelm@34485
   165
  }
wenzelm@34840
   166
}
wenzelm@34840
   167
wenzelm@34855
   168
wenzelm@34840
   169
class Document(
wenzelm@38150
   170
    val id: Document.Version_ID,
wenzelm@38150
   171
    val nodes: Map[String, Linear_Set[Command]],
wenzelm@38150
   172
    former_states: Map[Command, Command])  // FIXME !?
wenzelm@34840
   173
{
wenzelm@34859
   174
  /* command ranges */
wenzelm@34855
   175
wenzelm@38150
   176
  def commands(name: String): Linear_Set[Command] = nodes.get(name) getOrElse Linear_Set()
wenzelm@34855
   177
wenzelm@38150
   178
  def command_starts(name: String): Iterator[(Command, Int)] =
wenzelm@38150
   179
    Document.command_starts(commands(name).iterator)
wenzelm@38150
   180
wenzelm@38150
   181
  def command_start(name: String, cmd: Command): Option[Int] =
wenzelm@38150
   182
    command_starts(name).find(_._1 == cmd).map(_._2)
wenzelm@34855
   183
wenzelm@38150
   184
  def command_range(name: String, i: Int): Iterator[(Command, Int)] =
wenzelm@38150
   185
    command_starts(name) dropWhile { case (cmd, start) => start + cmd.length <= i }
wenzelm@34855
   186
wenzelm@38150
   187
  def command_range(name: String, i: Int, j: Int): Iterator[(Command, Int)] =
wenzelm@38150
   188
    command_range(name, i) takeWhile { case (_, start) => start < j }
wenzelm@34855
   189
wenzelm@38150
   190
  def command_at(name: String, i: Int): Option[(Command, Int)] =
wenzelm@34855
   191
  {
wenzelm@38150
   192
    val range = command_range(name, i)
wenzelm@34855
   193
    if (range.hasNext) Some(range.next) else None
wenzelm@34855
   194
  }
wenzelm@34855
   195
wenzelm@38150
   196
  def proper_command_at(name: String, i: Int): Option[Command] =
wenzelm@38150
   197
    command_at(name, i) match {
wenzelm@38150
   198
      case Some((command, _)) =>
wenzelm@38150
   199
        commands(name).reverse_iterator(command).find(cmd => !cmd.is_ignored)
wenzelm@37849
   200
      case None => None
wenzelm@37849
   201
    }
wenzelm@37849
   202
wenzelm@34855
   203
wenzelm@34855
   204
  /* command state assignment */
wenzelm@34840
   205
wenzelm@34840
   206
  val assignment = Future.promise[Map[Command, Command]]
wenzelm@34853
   207
  def await_assignment { assignment.join }
wenzelm@34840
   208
wenzelm@34859
   209
  @volatile private var tmp_states = former_states
wenzelm@34840
   210
wenzelm@34840
   211
  def assign_states(new_states: List[(Command, Command)])
wenzelm@34840
   212
  {
wenzelm@34840
   213
    assignment.fulfill(tmp_states ++ new_states)
wenzelm@34840
   214
    tmp_states = Map()
wenzelm@34840
   215
  }
wenzelm@34840
   216
wenzelm@36990
   217
  def current_state(cmd: Command): State =
wenzelm@34840
   218
  {
wenzelm@34840
   219
    require(assignment.is_finished)
wenzelm@36990
   220
    (assignment.join).get(cmd) match {
wenzelm@36990
   221
      case Some(cmd_state) => cmd_state.current_state
wenzelm@37186
   222
      case None => new State(cmd, Command.Status.UNDEFINED, 0, Nil, cmd.empty_markup)
wenzelm@36990
   223
    }
wenzelm@34840
   224
  }
wenzelm@34318
   225
}