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