src/Tools/jEdit/src/proofdocument/ProofDocument.scala
author wenzelm
Sun Sep 06 14:55:25 2009 +0200 (2009-09-06)
changeset 34712 4f0ee5ab0380
parent 34703 ff037c17332a
child 34722 8d41024ade63
permissions -rw-r--r--
replaced find_command_at by command_at -- null-free, proper Option;
tuned;
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@34703
    11
import scala.actors.Actor, Actor._
immler@34526
    12
import scala.collection.mutable.ListBuffer
wenzelm@34703
    13
wenzelm@34318
    14
import java.util.regex.Pattern
wenzelm@34703
    15
immler@34674
    16
import isabelle.prover.{Prover, Command, Command_State}
wenzelm@34318
    17
wenzelm@34485
    18
wenzelm@34483
    19
object ProofDocument
wenzelm@34483
    20
{
wenzelm@34582
    21
  // Be careful when changing this regex. Not only must it handle the
wenzelm@34318
    22
  // spurious end of a token but also:  
wenzelm@34318
    23
  // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
wenzelm@34318
    24
  // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
wenzelm@34318
    25
  
wenzelm@34483
    26
  val token_pattern = 
wenzelm@34318
    27
    Pattern.compile(
wenzelm@34318
    28
      "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
wenzelm@34318
    29
      "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
wenzelm@34318
    30
      "(\\?'?|')[A-Za-z_0-9.]*|" + 
wenzelm@34318
    31
      "[A-Za-z_0-9.]+|" + 
wenzelm@34318
    32
      "[!#$%&*+-/<=>?@^_|~]+|" +
wenzelm@34318
    33
      "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
wenzelm@34318
    34
      "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
wenzelm@34318
    35
      "[()\\[\\]{}:;]", Pattern.MULTILINE)
wenzelm@34485
    36
immler@34660
    37
  val empty =
immler@34660
    38
    new ProofDocument(isabelle.jedit.Isabelle.system.id(),
wenzelm@34689
    39
      Linear_Set(), Map(), Linear_Set(), Map(), _ => false,
immler@34674
    40
      actor(loop(react{case _ =>}))) // ignoring actor
immler@34660
    41
immler@34660
    42
  type StructureChange = List[(Option[Command], Option[Command])]
immler@34538
    43
wenzelm@34318
    44
}
wenzelm@34318
    45
wenzelm@34582
    46
class ProofDocument(
wenzelm@34582
    47
  val id: String,
wenzelm@34689
    48
  val tokens: Linear_Set[Token],
wenzelm@34582
    49
  val token_start: Map[Token, Int],
wenzelm@34689
    50
  val commands: Linear_Set[Command],
immler@34676
    51
  var states: Map[Command, Command_State],
immler@34674
    52
  is_command_keyword: String => Boolean,
immler@34674
    53
  change_receiver: Actor)
wenzelm@34483
    54
{
immler@34660
    55
  import ProofDocument.StructureChange
immler@34653
    56
immler@34532
    57
  def set_command_keyword(f: String => Boolean): ProofDocument =
immler@34674
    58
    new ProofDocument(id, tokens, token_start, commands, states, f, change_receiver)
immler@34674
    59
immler@34674
    60
  def set_change_receiver(cr: Actor): ProofDocument =
immler@34674
    61
    new ProofDocument(id, tokens, token_start, commands, states, is_command_keyword, cr)
wenzelm@34485
    62
wenzelm@34582
    63
  def content = Token.string_from_tokens(Nil ++ tokens, token_start)
wenzelm@34657
    64
wenzelm@34657
    65
wenzelm@34693
    66
  
wenzelm@34485
    67
  /** token view **/
wenzelm@34485
    68
wenzelm@34693
    69
  def text_changed(change: Change): (ProofDocument, StructureChange) =
wenzelm@34485
    70
  {
immler@34660
    71
    def edit_doc(doc_chgs: (ProofDocument, StructureChange), edit: Edit) = {
immler@34660
    72
      val (doc, chgs) = doc_chgs
wenzelm@34693
    73
      val (new_doc, chg) = doc.text_edit(edit, change.id)
immler@34660
    74
      (new_doc, chgs ++ chg)
immler@34660
    75
    }
wenzelm@34693
    76
    ((this, Nil: StructureChange) /: change.edits)(edit_doc)
immler@34660
    77
  }
immler@34660
    78
wenzelm@34693
    79
  def text_edit(e: Edit, id: String): (ProofDocument,StructureChange) =
immler@34660
    80
  {
immler@34660
    81
    case class TextChange(start: Int, added: String, removed: String)
immler@34660
    82
    val change = e match {
immler@34660
    83
      case Insert(s, a) => TextChange(s, a, "")
immler@34660
    84
      case Remove(s, r) => TextChange(s, "", r)
immler@34660
    85
    }
immler@34551
    86
    //indices of tokens
immler@34551
    87
    var start: Map[Token, Int] = token_start
immler@34551
    88
    def stop(t: Token) = start(t) + t.length
immler@34551
    89
    // split old token lists
wenzelm@34582
    90
    val tokens = Nil ++ this.tokens
immler@34551
    91
    val (begin, remaining) = tokens.span(stop(_) < change.start)
immler@34648
    92
    val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed.length)
immler@34551
    93
    // update indices
wenzelm@34582
    94
    start = end.foldLeft(start)((s, t) =>
immler@34648
    95
      s + (t -> (s(t) + change.added.length - change.removed.length)))
wenzelm@34485
    96
immler@34551
    97
    val split_begin = removed.takeWhile(start(_) < change.start).
immler@34554
    98
      map (t => {
immler@34554
    99
          val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind)
immler@34554
   100
          start += (split_tok -> start(t))
immler@34554
   101
          split_tok
immler@34554
   102
        })
immler@34554
   103
immler@34648
   104
    val split_end = removed.dropWhile(stop(_) < change.start + change.removed.length).
immler@34554
   105
      map (t => {
wenzelm@34582
   106
          val split_tok =
immler@34648
   107
            new Token(t.content.substring(change.start + change.removed.length - start(t)), t.kind)
immler@34554
   108
          start += (split_tok -> start(t))
immler@34554
   109
          split_tok
immler@34554
   110
        })
immler@34551
   111
    // update indices
immler@34554
   112
    start = removed.foldLeft (start) ((s, t) => s - t)
immler@34554
   113
    start = split_end.foldLeft (start) ((s, t) =>
immler@34554
   114
    s + (t -> (change.start + change.added.length)))
wenzelm@34318
   115
immler@34551
   116
    val ins = new Token(change.added, Token.Kind.OTHER)
immler@34551
   117
    start += (ins -> change.start)
immler@34551
   118
    
wenzelm@34582
   119
    var invalid_tokens = split_begin ::: ins :: split_end ::: end
wenzelm@34582
   120
    var new_tokens: List[Token] = Nil
wenzelm@34582
   121
    var old_suffix: List[Token] = Nil
wenzelm@34318
   122
immler@34551
   123
    val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
wenzelm@34582
   124
    val matcher =
wenzelm@34582
   125
      ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
immler@34526
   126
immler@34526
   127
    while (matcher.find() && invalid_tokens != Nil) {
wenzelm@34485
   128
			val kind =
wenzelm@34505
   129
        if (is_command_keyword(matcher.group))
wenzelm@34485
   130
          Token.Kind.COMMAND_START
wenzelm@34494
   131
        else if (matcher.end - matcher.start > 2 && matcher.group.substring(0, 2) == "(*")
wenzelm@34485
   132
          Token.Kind.COMMENT
wenzelm@34485
   133
        else
wenzelm@34485
   134
          Token.Kind.OTHER
immler@34551
   135
      val new_token = new Token(matcher.group, kind)
immler@34551
   136
      start += (new_token -> (match_start + matcher.start))
immler@34526
   137
      new_tokens ::= new_token
wenzelm@34318
   138
immler@34660
   139
      invalid_tokens = invalid_tokens dropWhile (stop(_) < stop(new_token))
immler@34526
   140
      invalid_tokens match {
wenzelm@34582
   141
        case t :: ts =>
wenzelm@34582
   142
          if (start(t) == start(new_token) &&
wenzelm@34582
   143
              start(t) > change.start + change.added.length) {
immler@34597
   144
          old_suffix = t :: ts
immler@34592
   145
          new_tokens = new_tokens.tail
immler@34526
   146
          invalid_tokens = Nil
immler@34526
   147
        }
immler@34526
   148
        case _ =>
wenzelm@34318
   149
      }
wenzelm@34318
   150
    }
immler@34526
   151
    val insert = new_tokens.reverse
immler@34544
   152
    val new_token_list = begin ::: insert ::: old_suffix
immler@34660
   153
    token_changed(id, begin.lastOption, insert,
immler@34597
   154
      old_suffix.firstOption, new_token_list, start)
wenzelm@34318
   155
  }
wenzelm@34582
   156
wenzelm@34318
   157
  
wenzelm@34485
   158
  /** command view **/
wenzelm@34485
   159
wenzelm@34582
   160
  private def token_changed(
wenzelm@34582
   161
    new_id: String,
wenzelm@34582
   162
    before_change: Option[Token],
wenzelm@34582
   163
    inserted_tokens: List[Token],
wenzelm@34582
   164
    after_change: Option[Token],
immler@34597
   165
    new_tokens: List[Token],
immler@34660
   166
    new_token_start: Map[Token, Int]):
immler@34660
   167
  (ProofDocument, StructureChange) =
wenzelm@34485
   168
  {
wenzelm@34689
   169
    val new_tokenset = Linear_Set[Token]() ++ new_tokens
immler@34593
   170
    val cmd_before_change = before_change match {
immler@34593
   171
      case None => None
immler@34593
   172
      case Some(bc) =>
immler@34593
   173
        val cmd_with_bc = commands.find(_.contains(bc)).get
immler@34593
   174
        if (cmd_with_bc.tokens.last == bc) {
immler@34593
   175
          if (new_tokenset.next(bc).map(_.is_start).getOrElse(true))
immler@34593
   176
            Some(cmd_with_bc)
immler@34593
   177
          else commands.prev(cmd_with_bc)
immler@34593
   178
        }
immler@34593
   179
        else commands.prev(cmd_with_bc)
immler@34593
   180
    }
immler@34544
   181
immler@34593
   182
    val cmd_after_change = after_change match {
immler@34593
   183
      case None => None
immler@34593
   184
      case Some(ac) =>
immler@34593
   185
        val cmd_with_ac = commands.find(_.contains(ac)).get
immler@34593
   186
        if (ac.is_start)
immler@34593
   187
          Some(cmd_with_ac)
immler@34593
   188
        else
immler@34593
   189
          commands.next(cmd_with_ac)
immler@34593
   190
    }
wenzelm@34485
   191
immler@34593
   192
    val removed_commands = commands.dropWhile(Some(_) != cmd_before_change).drop(1).
immler@34554
   193
      takeWhile(Some(_) != cmd_after_change)
immler@34554
   194
immler@34554
   195
    // calculate inserted commands
immler@34526
   196
    def tokens_to_commands(tokens: List[Token]): List[Command]= {
immler@34526
   197
      tokens match {
immler@34526
   198
        case Nil => Nil
wenzelm@34582
   199
        case t :: ts =>
wenzelm@34582
   200
          val (cmd, rest) =
wenzelm@34582
   201
            ts.span(t => t.kind != Token.Kind.COMMAND_START && t.kind != Token.Kind.COMMENT)
immler@34674
   202
          new Command(t :: cmd, new_token_start, change_receiver) :: tokens_to_commands(rest)
wenzelm@34485
   203
      }
wenzelm@34485
   204
    }
wenzelm@34485
   205
immler@34593
   206
    val split_begin =
immler@34593
   207
      if (before_change.isDefined) {
immler@34593
   208
        val changed =
immler@34593
   209
          if (cmd_before_change.isDefined)
immler@34595
   210
            new_tokens.dropWhile(_ != cmd_before_change.get.tokens.last).drop(1)
immler@34593
   211
          else new_tokenset
immler@34593
   212
        if (changed.exists(_ == before_change.get))
immler@34597
   213
          changed.takeWhile(_ != before_change.get).toList :::
immler@34597
   214
            List(before_change.get)
immler@34593
   215
        else Nil
immler@34593
   216
      } else Nil
immler@34554
   217
immler@34593
   218
    val split_end =
immler@34667
   219
      if (after_change.isDefined) {
immler@34595
   220
        val unchanged = new_tokens.dropWhile(_ != after_change.get)
immler@34667
   221
        if(cmd_after_change.isDefined) {
immler@34667
   222
          if (unchanged.exists(_ == cmd_after_change.get.tokens.first))
immler@34667
   223
            unchanged.takeWhile(_ != cmd_after_change.get.tokens.first).toList
immler@34667
   224
          else Nil
immler@34667
   225
        } else {
immler@34667
   226
          unchanged
immler@34667
   227
        }
immler@34593
   228
      } else Nil
immler@34593
   229
immler@34597
   230
    val rescan_begin =
immler@34597
   231
      split_begin :::
immler@34597
   232
        before_change.map(bc => new_tokens.dropWhile(_ != bc).drop(1)).getOrElse(new_tokens)
wenzelm@34582
   233
    val rescanning_tokens =
immler@34597
   234
      after_change.map(ac => rescan_begin.takeWhile(_ != ac)).getOrElse(rescan_begin) :::
immler@34597
   235
        split_end
immler@34593
   236
    val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
immler@34554
   237
immler@34550
   238
    // build new document
immler@34554
   239
    val new_commandset = commands.delete_between(cmd_before_change, cmd_after_change).
immler@34554
   240
        insert_after(cmd_before_change, inserted_commands)
immler@34554
   241
immler@34544
   242
    val doc =
immler@34674
   243
      new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
immler@34674
   244
        states -- removed_commands, is_command_keyword, change_receiver)
immler@34660
   245
immler@34660
   246
    val removes =
immler@34660
   247
      for (cmd <- removed_commands) yield (cmd_before_change -> None)
immler@34660
   248
    val inserts =
immler@34660
   249
      for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd))
immler@34660
   250
immler@34660
   251
    return (doc, removes.toList ++ inserts)
wenzelm@34485
   252
  }
immler@34596
   253
immler@34596
   254
  val commands_offsets = {
immler@34596
   255
    var last_stop = 0
immler@34596
   256
    (for (c <- commands) yield {
immler@34596
   257
      val r = c -> (last_stop,c.stop(this))
immler@34596
   258
      last_stop = c.stop(this)
immler@34596
   259
      r
immler@34596
   260
    }).toArray
immler@34596
   261
  }
immler@34596
   262
wenzelm@34712
   263
  def command_at(pos: Int): Option[Command] =
wenzelm@34712
   264
    find_command(pos, 0, commands_offsets.length)
wenzelm@34712
   265
immler@34596
   266
  // use a binary search to find commands for a given offset
wenzelm@34712
   267
  private def find_command(pos: Int, array_start: Int, array_stop: Int): Option[Command] =
wenzelm@34712
   268
  {
immler@34596
   269
    val middle_index = (array_start + array_stop) / 2
wenzelm@34712
   270
    if (middle_index >= commands_offsets.length) return None
immler@34596
   271
    val (middle, (start, stop)) = commands_offsets(middle_index)
immler@34596
   272
    // does middle contain pos?
wenzelm@34712
   273
    if (start <= pos && pos < stop)
wenzelm@34712
   274
      Some(middle)
immler@34596
   275
    else if (start > pos)
wenzelm@34712
   276
      find_command(pos, array_start, middle_index)
immler@34596
   277
    else if (stop <= pos)
wenzelm@34712
   278
      find_command(pos, middle_index + 1, array_stop)
wenzelm@34712
   279
    else error("impossible")
immler@34596
   280
  }
wenzelm@34318
   281
}