src/Tools/jEdit/src/proofdocument/document.scala
author wenzelm
Fri Jan 01 17:29:35 2010 +0100 (2010-01-01)
changeset 34824 ac35eee85f5c
parent 34823 2f3ea37c5958
child 34825 7f72547f9b12
permissions -rw-r--r--
renamed current_document to recent_document (might be a bit older than current_change);
Change: explicit future value of Document.Change instead of implicit lookup in Session database;
Document_Model: apply Document.text_edits here (as future);
wenzelm@34407
     1
/*
wenzelm@34485
     2
 * Document as list of commands, consisting of lists of tokens
wenzelm@34407
     3
 *
wenzelm@34407
     4
 * @author Johannes Hölzl, TU Munich
immler@34532
     5
 * @author Fabian Immler, TU Munich
wenzelm@34485
     6
 * @author Makarius
wenzelm@34407
     7
 */
wenzelm@34407
     8
wenzelm@34318
     9
package isabelle.proofdocument
wenzelm@34318
    10
wenzelm@34760
    11
wenzelm@34824
    12
import scala.actors.Future
wenzelm@34824
    13
import scala.actors.Futures._
wenzelm@34818
    14
import scala.actors.Actor._
wenzelm@34824
    15
import scala.collection.mutable
wenzelm@34818
    16
wenzelm@34318
    17
import java.util.regex.Pattern
wenzelm@34703
    18
wenzelm@34318
    19
wenzelm@34823
    20
object Document
wenzelm@34483
    21
{
wenzelm@34582
    22
  // Be careful when changing this regex. Not only must it handle the
wenzelm@34818
    23
  // spurious end of a token but also:
wenzelm@34318
    24
  // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
wenzelm@34318
    25
  // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
wenzelm@34818
    26
wenzelm@34818
    27
  val token_pattern =
wenzelm@34318
    28
    Pattern.compile(
wenzelm@34318
    29
      "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
wenzelm@34318
    30
      "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
wenzelm@34818
    31
      "(\\?'?|')[A-Za-z_0-9.]*|" +
wenzelm@34818
    32
      "[A-Za-z_0-9.]+|" +
wenzelm@34318
    33
      "[!#$%&*+-/<=>?@^_|~]+|" +
wenzelm@34318
    34
      "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
wenzelm@34318
    35
      "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
wenzelm@34318
    36
      "[()\\[\\]{}:;]", Pattern.MULTILINE)
wenzelm@34485
    37
wenzelm@34823
    38
  def empty(id: Isar_Document.Document_ID): Document =
wenzelm@34823
    39
    new Document(id, Linear_Set(), Map(), Linear_Set(), Map())
immler@34660
    40
wenzelm@34824
    41
  type Structure_Edit = (Option[Command], Option[Command])
wenzelm@34824
    42
  type Structure_Change = List[Structure_Edit]
wenzelm@34824
    43
  type Result = (Document, List[Structure_Edit])
wenzelm@34824
    44
wenzelm@34824
    45
  def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
wenzelm@34824
    46
    edits: List[Edit]): Result =
wenzelm@34824
    47
  {
wenzelm@34824
    48
    val changes = new mutable.ListBuffer[Structure_Edit]
wenzelm@34824
    49
    val new_doc = (old_doc /: edits)((doc1: Document, edit: Edit) =>
wenzelm@34824
    50
      {
wenzelm@34824
    51
        val (doc2, chgs) = doc1.text_edit(session, edit, new_id)  // FIXME odd multiple use of id
wenzelm@34824
    52
        changes ++ chgs
wenzelm@34824
    53
        doc2
wenzelm@34824
    54
      })
wenzelm@34824
    55
    (new_doc, changes.toList)
wenzelm@34824
    56
  }
wenzelm@34778
    57
}
immler@34538
    58
wenzelm@34318
    59
wenzelm@34823
    60
class Document(
wenzelm@34818
    61
    val id: Isar_Document.Document_ID,
wenzelm@34818
    62
    val tokens: Linear_Set[Token],   // FIXME plain List, inside Command
wenzelm@34818
    63
    val token_start: Map[Token, Int],  // FIXME eliminate
wenzelm@34818
    64
    val commands: Linear_Set[Command],
wenzelm@34818
    65
    var states: Map[Command, Command])   // FIXME immutable, eliminate!?
wenzelm@34818
    66
  extends Session.Entity
wenzelm@34483
    67
{
wenzelm@34582
    68
  def content = Token.string_from_tokens(Nil ++ tokens, token_start)
wenzelm@34657
    69
wenzelm@34657
    70
wenzelm@34818
    71
  /* accumulated messages */
wenzelm@34818
    72
wenzelm@34818
    73
  private val accumulator = actor {
wenzelm@34818
    74
    loop {
wenzelm@34818
    75
      react {
wenzelm@34818
    76
        case (session: Session, message: XML.Tree) =>
wenzelm@34818
    77
          message match {
wenzelm@34818
    78
            case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
wenzelm@34818
    79
              for {
wenzelm@34818
    80
                XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
wenzelm@34818
    81
                  <- elems
wenzelm@34818
    82
              } {
wenzelm@34818
    83
                session.lookup_entity(cmd_id) match {
wenzelm@34818
    84
                  case Some(cmd: Command) =>
wenzelm@34824
    85
                    val state = cmd.finish_static(state_id)   // FIXME more explicit typing
wenzelm@34818
    86
                    session.register_entity(state)
wenzelm@34818
    87
                    states += (cmd -> state)  // FIXME !?
wenzelm@34818
    88
                    session.command_change.event(cmd)   // FIXME really!?
wenzelm@34818
    89
                  case _ =>
wenzelm@34818
    90
                }
wenzelm@34818
    91
              }
wenzelm@34818
    92
            case _ =>
wenzelm@34818
    93
          }
wenzelm@34818
    94
wenzelm@34818
    95
        case bad => System.err.println("document accumulator: ignoring bad message " + bad)
wenzelm@34818
    96
      }
wenzelm@34818
    97
    }
wenzelm@34818
    98
  }
wenzelm@34818
    99
wenzelm@34818
   100
  def consume(session: Session, message: XML.Tree) { accumulator ! (session, message) }
wenzelm@34818
   101
wenzelm@34818
   102
wenzelm@34818
   103
wenzelm@34485
   104
  /** token view **/
wenzelm@34485
   105
wenzelm@34824
   106
  def text_edit(session: Session, e: Edit, id: String): Document.Result =
immler@34660
   107
  {
immler@34660
   108
    case class TextChange(start: Int, added: String, removed: String)
immler@34660
   109
    val change = e match {
immler@34660
   110
      case Insert(s, a) => TextChange(s, a, "")
immler@34660
   111
      case Remove(s, r) => TextChange(s, "", r)
immler@34660
   112
    }
immler@34551
   113
    //indices of tokens
immler@34551
   114
    var start: Map[Token, Int] = token_start
immler@34551
   115
    def stop(t: Token) = start(t) + t.length
immler@34551
   116
    // split old token lists
wenzelm@34582
   117
    val tokens = Nil ++ this.tokens
immler@34551
   118
    val (begin, remaining) = tokens.span(stop(_) < change.start)
immler@34648
   119
    val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed.length)
immler@34551
   120
    // update indices
wenzelm@34582
   121
    start = end.foldLeft(start)((s, t) =>
immler@34648
   122
      s + (t -> (s(t) + change.added.length - change.removed.length)))
wenzelm@34485
   123
immler@34551
   124
    val split_begin = removed.takeWhile(start(_) < change.start).
immler@34554
   125
      map (t => {
immler@34554
   126
          val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind)
immler@34554
   127
          start += (split_tok -> start(t))
immler@34554
   128
          split_tok
immler@34554
   129
        })
immler@34554
   130
immler@34648
   131
    val split_end = removed.dropWhile(stop(_) < change.start + change.removed.length).
immler@34554
   132
      map (t => {
wenzelm@34582
   133
          val split_tok =
immler@34648
   134
            new Token(t.content.substring(change.start + change.removed.length - start(t)), t.kind)
immler@34554
   135
          start += (split_tok -> start(t))
immler@34554
   136
          split_tok
immler@34554
   137
        })
immler@34551
   138
    // update indices
immler@34554
   139
    start = removed.foldLeft (start) ((s, t) => s - t)
immler@34554
   140
    start = split_end.foldLeft (start) ((s, t) =>
immler@34554
   141
    s + (t -> (change.start + change.added.length)))
wenzelm@34318
   142
immler@34551
   143
    val ins = new Token(change.added, Token.Kind.OTHER)
immler@34551
   144
    start += (ins -> change.start)
wenzelm@34818
   145
wenzelm@34582
   146
    var invalid_tokens = split_begin ::: ins :: split_end ::: end
wenzelm@34582
   147
    var new_tokens: List[Token] = Nil
wenzelm@34582
   148
    var old_suffix: List[Token] = Nil
wenzelm@34318
   149
immler@34551
   150
    val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
wenzelm@34582
   151
    val matcher =
wenzelm@34823
   152
      Document.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
immler@34526
   153
immler@34526
   154
    while (matcher.find() && invalid_tokens != Nil) {
wenzelm@34485
   155
			val kind =
wenzelm@34819
   156
        if (session.current_syntax.is_command(matcher.group))
wenzelm@34485
   157
          Token.Kind.COMMAND_START
wenzelm@34494
   158
        else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
wenzelm@34485
   159
          Token.Kind.COMMENT
wenzelm@34485
   160
        else
wenzelm@34485
   161
          Token.Kind.OTHER
immler@34551
   162
      val new_token = new Token(matcher.group, kind)
immler@34551
   163
      start += (new_token -> (match_start + matcher.start))
immler@34526
   164
      new_tokens ::= new_token
wenzelm@34318
   165
immler@34660
   166
      invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token))
immler@34526
   167
      invalid_tokens match {
wenzelm@34582
   168
        case t :: ts =>
wenzelm@34582
   169
          if (start(t) == start(new_token) &&
wenzelm@34582
   170
              start(t) > change.start + change.added.length) {
immler@34597
   171
          old_suffix = t :: ts
immler@34592
   172
          new_tokens = new_tokens.tail
immler@34526
   173
          invalid_tokens = Nil
immler@34526
   174
        }
immler@34526
   175
        case _ =>
wenzelm@34318
   176
      }
wenzelm@34318
   177
    }
immler@34526
   178
    val insert = new_tokens.reverse
immler@34544
   179
    val new_token_list = begin ::: insert ::: old_suffix
wenzelm@34778
   180
    token_changed(session, id, begin.lastOption, insert,
immler@34597
   181
      old_suffix.firstOption, new_token_list, start)
wenzelm@34318
   182
  }
wenzelm@34582
   183
wenzelm@34818
   184
wenzelm@34485
   185
  /** command view **/
wenzelm@34485
   186
wenzelm@34582
   187
  private def token_changed(
wenzelm@34824
   188
      session: Session,
wenzelm@34824
   189
      new_id: String,
wenzelm@34824
   190
      before_change: Option[Token],
wenzelm@34824
   191
      inserted_tokens: List[Token],
wenzelm@34824
   192
      after_change: Option[Token],
wenzelm@34824
   193
      new_tokens: List[Token],
wenzelm@34824
   194
      new_token_start: Map[Token, Int]):
wenzelm@34824
   195
    Document.Result =
wenzelm@34485
   196
  {
wenzelm@34689
   197
    val new_tokenset = Linear_Set[Token]() ++ new_tokens
immler@34593
   198
    val cmd_before_change = before_change match {
immler@34593
   199
      case None => None
immler@34593
   200
      case Some(bc) =>
immler@34593
   201
        val cmd_with_bc = commands.find(_.contains(bc)).get
immler@34593
   202
        if (cmd_with_bc.tokens.last == bc) {
immler@34593
   203
          if (new_tokenset.next(bc).map(_.is_start).getOrElse(true))
immler@34593
   204
            Some(cmd_with_bc)
immler@34593
   205
          else commands.prev(cmd_with_bc)
immler@34593
   206
        }
immler@34593
   207
        else commands.prev(cmd_with_bc)
immler@34593
   208
    }
immler@34544
   209
immler@34593
   210
    val cmd_after_change = after_change match {
immler@34593
   211
      case None => None
immler@34593
   212
      case Some(ac) =>
immler@34593
   213
        val cmd_with_ac = commands.find(_.contains(ac)).get
immler@34593
   214
        if (ac.is_start)
immler@34593
   215
          Some(cmd_with_ac)
immler@34593
   216
        else
immler@34593
   217
          commands.next(cmd_with_ac)
immler@34593
   218
    }
wenzelm@34485
   219
immler@34593
   220
    val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1).
immler@34554
   221
      takeWhile(Some(_) != cmd_after_change)
immler@34554
   222
immler@34554
   223
    // calculate inserted commands
immler@34526
   224
    def tokens_to_commands(tokens: List[Token]): List[Command]= {
immler@34526
   225
      tokens match {
immler@34526
   226
        case Nil => Nil
wenzelm@34582
   227
        case t :: ts =>
wenzelm@34582
   228
          val (cmd, rest) =
wenzelm@34582
   229
            ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
wenzelm@34778
   230
          new Command(session.create_id(), t :: cmd, new_token_start) :: tokens_to_commands(rest)
wenzelm@34485
   231
      }
wenzelm@34485
   232
    }
wenzelm@34485
   233
immler@34593
   234
    val split_begin =
immler@34593
   235
      if (before_change.isDefined) {
immler@34593
   236
        val changed =
immler@34593
   237
          if (cmd_before_change.isDefined)
immler@34595
   238
            new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1)
immler@34593
   239
          else new_tokenset
immler@34593
   240
        if (changed.exists(_ == before_change.get))
immler@34597
   241
          changed.takeWhile(_ != before_change.get).toList :::
immler@34597
   242
            List(before_change.get)
immler@34593
   243
        else Nil
immler@34593
   244
      } else Nil
immler@34554
   245
immler@34593
   246
    val split_end =
immler@34667
   247
      if (after_change.isDefined) {
immler@34595
   248
        val unchanged = new_tokens.dropWhile(_ != after_change.get)
immler@34667
   249
        if(cmd_after_change.isDefined) {
immler@34667
   250
          if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
immler@34667
   251
            unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
immler@34667
   252
          else Nil
immler@34667
   253
        } else {
immler@34667
   254
          unchanged
immler@34667
   255
        }
immler@34593
   256
      } else Nil
immler@34593
   257
immler@34597
   258
    val rescan_begin =
immler@34597
   259
      split_begin :::
immler@34597
   260
        before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens)
wenzelm@34582
   261
    val rescanning_tokens =
immler@34597
   262
      after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) :::
immler@34597
   263
        split_end
immler@34593
   264
    val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
immler@34554
   265
immler@34550
   266
    // build new document
wenzelm@34739
   267
    val new_commandset = commands.
wenzelm@34739
   268
      delete_between(cmd_before_change, cmd_after_change).
wenzelm@34739
   269
      append_after(cmd_before_change, inserted_commands)
wenzelm@34739
   270
immler@34554
   271
immler@34544
   272
    val doc =
wenzelm@34823
   273
      new Document(new_id, new_tokenset, new_token_start, new_commandset,
wenzelm@34778
   274
        states -- removed_commands)
immler@34660
   275
immler@34660
   276
    val removes =
immler@34660
   277
      for (cmd <- removed_commands) yield (cmd_before_change -> None)
immler@34660
   278
    val inserts =
immler@34660
   279
      for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd))
immler@34660
   280
immler@34660
   281
    return (doc, removes.toList ++ inserts)
wenzelm@34485
   282
  }
immler@34596
   283
immler@34596
   284
  val commands_offsets = {
immler@34596
   285
    var last_stop = 0
immler@34596
   286
    (for (c <- commands) yield {
wenzelm@34824
   287
      val r = c -> (last_stop, c.stop(this))
immler@34596
   288
      last_stop = c.stop(this)
immler@34596
   289
      r
immler@34596
   290
    }).toArray
immler@34596
   291
  }
immler@34596
   292
wenzelm@34712
   293
  def command_at(pos: Int): Option[Command] =
wenzelm@34712
   294
    find_command(pos, 0, commands_offsets.length)
wenzelm@34712
   295
immler@34596
   296
  // use a binary search to find commands for a given offset
wenzelm@34712
   297
  private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] =
wenzelm@34712
   298
  {
immler@34596
   299
    val middle_index = (array_start + array_stop) / 2
wenzelm@34712
   300
    if (middle_index >= commands_offsets.length) return None
immler@34596
   301
    val (middle, (start, stop)) = commands_offsets(middle_index)
immler@34596
   302
    // does middle contain pos?
wenzelm@34712
   303
    if (start <= pos && pos < stop)
wenzelm@34712
   304
      Some(middle)
immler@34596
   305
    else if (start > pos)
wenzelm@34712
   306
      find_command(pos, array_start, middle_index)
immler@34596
   307
    else if (stop <= pos)
wenzelm@34712
   308
      find_command(pos, middle_index + 1, array_stop)
wenzelm@34712
   309
    else error("impossible")
immler@34596
   310
  }
wenzelm@34318
   311
}