src/Tools/jEdit/src/proofdocument/ProofDocument.scala
author wenzelm
Mon Jan 19 23:29:44 2009 +0100 (2009-01-19 ago)
changeset 34485 6475bfb4ff99
parent 34483 0923926022d7
child 34491 20e9d420dbbb
permissions -rw-r--r--
joined Document with ProofDocument;
misc tuning;
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
wenzelm@34485
     5
 * @author Makarius
wenzelm@34407
     6
 */
wenzelm@34407
     7
wenzelm@34318
     8
package isabelle.proofdocument
wenzelm@34318
     9
wenzelm@34483
    10
wenzelm@34318
    11
import java.util.regex.Pattern
wenzelm@34485
    12
import isabelle.prover.{Prover, Command}
wenzelm@34318
    13
wenzelm@34318
    14
wenzelm@34485
    15
class StructureChange(
wenzelm@34485
    16
  val beforeChange: Command,
wenzelm@34485
    17
  val addedCommands: List[Command],
wenzelm@34485
    18
  val removedCommands: List[Command])
wenzelm@34485
    19
wenzelm@34483
    20
object ProofDocument
wenzelm@34483
    21
{
wenzelm@34485
    22
  // Be carefully when changing this regex. Not only must it handle the 
wenzelm@34318
    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@34318
    26
  
wenzelm@34483
    27
  val token_pattern = 
wenzelm@34318
    28
    Pattern.compile(
wenzelm@34318
    29
      "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
wenzelm@34318
    30
      "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
wenzelm@34318
    31
      "(\\?'?|')[A-Za-z_0-9.]*|" + 
wenzelm@34318
    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@34318
    38
}
wenzelm@34318
    39
wenzelm@34485
    40
class ProofDocument(text: Text, prover: Prover)
wenzelm@34483
    41
{
wenzelm@34318
    42
  private var active = false 
wenzelm@34456
    43
  def activate() {
wenzelm@34456
    44
    if (!active) {
wenzelm@34318
    45
      active = true
wenzelm@34485
    46
      text_changed(0, text.length, 0)
wenzelm@34318
    47
    }
wenzelm@34456
    48
  }
wenzelm@34485
    49
wenzelm@34485
    50
  text.changes += (changed => text_changed(changed.start, changed.added, changed.removed))
wenzelm@34485
    51
wenzelm@34485
    52
wenzelm@34485
    53
wenzelm@34485
    54
  /** token view **/
wenzelm@34485
    55
wenzelm@34485
    56
  protected var firstToken: Token = null
wenzelm@34485
    57
  protected var lastToken: Token = null
wenzelm@34318
    58
  
wenzelm@34485
    59
  protected def tokens(start: Token, stop: Token) = new Iterator[Token] {
wenzelm@34318
    60
      var current = start
wenzelm@34483
    61
      def hasNext = current != stop && current != null
wenzelm@34318
    62
      def next() = { val save = current ; current = current.next ; save }
wenzelm@34318
    63
    }
wenzelm@34485
    64
  protected def tokens(start: Token): Iterator[Token] = tokens(start, null)
wenzelm@34485
    65
  protected def tokens() : Iterator[Token] = tokens(firstToken, null)
wenzelm@34485
    66
wenzelm@34318
    67
wenzelm@34485
    68
  private def text_changed(start: Int, addedLen: Int, removedLen: Int)
wenzelm@34485
    69
  {
wenzelm@34485
    70
    if (!active)
wenzelm@34318
    71
      return
wenzelm@34485
    72
wenzelm@34318
    73
    var beforeChange = 
wenzelm@34485
    74
      if (Token.check_stop(firstToken, _ < start)) Token.scan(firstToken, _.stop >= start)
wenzelm@34318
    75
      else null
wenzelm@34318
    76
    
wenzelm@34318
    77
    var firstRemoved = 
wenzelm@34318
    78
      if (beforeChange != null) beforeChange.next
wenzelm@34485
    79
      else if (Token.check_start(firstToken, _ <= start + removedLen)) firstToken
wenzelm@34318
    80
      else null 
wenzelm@34318
    81
wenzelm@34485
    82
    var lastRemoved = Token.scan(firstRemoved, _.start > start + removedLen)
wenzelm@34318
    83
wenzelm@34318
    84
    var shiftToken = 
wenzelm@34318
    85
      if (lastRemoved != null) lastRemoved
wenzelm@34485
    86
      else if (Token.check_start(firstToken, _ > start)) firstToken
wenzelm@34318
    87
      else null
wenzelm@34318
    88
    
wenzelm@34485
    89
    while (shiftToken != null) {
wenzelm@34318
    90
      shiftToken.shift(addedLen - removedLen, start)
wenzelm@34318
    91
      shiftToken = shiftToken.next
wenzelm@34318
    92
    }
wenzelm@34318
    93
    
wenzelm@34318
    94
    // scan changed tokens until the end of the text or a matching token is
wenzelm@34318
    95
    // found which is beyond the changed area
wenzelm@34318
    96
    val matchStart = if (beforeChange == null) 0 else beforeChange.stop
wenzelm@34483
    97
    var firstAdded: Token = null
wenzelm@34483
    98
    var lastAdded: Token = null
wenzelm@34318
    99
wenzelm@34483
   100
    val matcher = ProofDocument.token_pattern.matcher(text.content(matchStart, text.length))
wenzelm@34318
   101
    var finished = false
wenzelm@34318
   102
    var position = 0 
wenzelm@34483
   103
    while (matcher.find(position) && ! finished) {
wenzelm@34318
   104
      position = matcher.end()
wenzelm@34485
   105
			val kind =
wenzelm@34485
   106
        if (prover.is_command_keyword(matcher.group()))
wenzelm@34485
   107
          Token.Kind.COMMAND_START
wenzelm@34485
   108
        else if (matcher.end() - matcher.start() > 2 && matcher.group().substring(0, 2) == "(*")
wenzelm@34485
   109
          Token.Kind.COMMENT
wenzelm@34485
   110
        else
wenzelm@34485
   111
          Token.Kind.OTHER
wenzelm@34481
   112
      val newToken = new Token(matcher.start() + matchStart, matcher.end() + matchStart, kind)
wenzelm@34318
   113
wenzelm@34318
   114
      if (firstAdded == null)
wenzelm@34318
   115
        firstAdded = newToken
wenzelm@34318
   116
      else {
wenzelm@34483
   117
        newToken.prev = lastAdded
wenzelm@34318
   118
        lastAdded.next = newToken
wenzelm@34318
   119
      }
wenzelm@34318
   120
      lastAdded = newToken
wenzelm@34318
   121
      
wenzelm@34485
   122
      while (Token.check_stop(lastRemoved, _ < newToken.stop) &&
wenzelm@34318
   123
              lastRemoved.next != null)	
wenzelm@34318
   124
        lastRemoved = lastRemoved.next
wenzelm@34318
   125
			
wenzelm@34318
   126
      if (newToken.stop >= start + addedLen && 
wenzelm@34485
   127
            Token.check_stop(lastRemoved, _ == newToken.stop))
wenzelm@34318
   128
        finished = true
wenzelm@34318
   129
    }
wenzelm@34318
   130
wenzelm@34318
   131
    var afterChange = if (lastRemoved != null) lastRemoved.next else null
wenzelm@34318
   132
		
wenzelm@34318
   133
    // remove superflous first token-change
wenzelm@34318
   134
    if (firstAdded != null && firstAdded == firstRemoved && 
wenzelm@34318
   135
          firstAdded.stop < start) {
wenzelm@34318
   136
      beforeChange = firstRemoved
wenzelm@34318
   137
      if (lastRemoved == firstRemoved) {
wenzelm@34318
   138
        lastRemoved = null
wenzelm@34318
   139
        firstRemoved = null
wenzelm@34318
   140
      }
wenzelm@34318
   141
      else {
wenzelm@34318
   142
        firstRemoved = firstRemoved.next
wenzelm@34318
   143
        assert(firstRemoved != null)
wenzelm@34318
   144
      }
wenzelm@34318
   145
wenzelm@34318
   146
      if (lastAdded == firstAdded) {
wenzelm@34318
   147
        lastAdded = null
wenzelm@34318
   148
        firstAdded = null
wenzelm@34318
   149
      }
wenzelm@34318
   150
      if (firstAdded != null)
wenzelm@34318
   151
        firstAdded = firstAdded.next
wenzelm@34318
   152
    }
wenzelm@34318
   153
    
wenzelm@34318
   154
    // remove superflous last token-change
wenzelm@34318
   155
    if (lastAdded != null && lastAdded == lastRemoved &&
wenzelm@34318
   156
          lastAdded.start > start + addedLen) {
wenzelm@34318
   157
      afterChange = lastRemoved
wenzelm@34318
   158
      if (firstRemoved == lastRemoved) {
wenzelm@34318
   159
        firstRemoved = null
wenzelm@34318
   160
        lastRemoved = null
wenzelm@34318
   161
      }
wenzelm@34318
   162
      else {
wenzelm@34483
   163
        lastRemoved = lastRemoved.prev
wenzelm@34318
   164
        assert(lastRemoved != null)
wenzelm@34318
   165
      }
wenzelm@34318
   166
      
wenzelm@34318
   167
      if (lastAdded == firstAdded) {
wenzelm@34318
   168
        lastAdded = null
wenzelm@34318
   169
        firstAdded = null
wenzelm@34318
   170
      }
wenzelm@34318
   171
      else
wenzelm@34483
   172
        lastAdded = lastAdded.prev
wenzelm@34318
   173
    }
wenzelm@34318
   174
    
wenzelm@34318
   175
    if (firstRemoved == null && firstAdded == null)
wenzelm@34318
   176
      return
wenzelm@34318
   177
    
wenzelm@34318
   178
    if (firstToken == null) {
wenzelm@34318
   179
      firstToken = firstAdded
wenzelm@34318
   180
      lastToken = lastAdded
wenzelm@34318
   181
    }
wenzelm@34318
   182
    else {
wenzelm@34318
   183
      // cut removed tokens out of list
wenzelm@34318
   184
      if (firstRemoved != null)
wenzelm@34483
   185
        firstRemoved.prev = null
wenzelm@34318
   186
      if (lastRemoved != null)
wenzelm@34318
   187
        lastRemoved.next = null
wenzelm@34318
   188
      
wenzelm@34318
   189
      if (firstToken == firstRemoved)
wenzelm@34318
   190
        if (firstAdded != null)
wenzelm@34318
   191
          firstToken = firstAdded
wenzelm@34318
   192
        else
wenzelm@34318
   193
          firstToken = afterChange
wenzelm@34318
   194
      
wenzelm@34318
   195
      if (lastToken == lastRemoved)
wenzelm@34318
   196
        if (lastAdded != null)
wenzelm@34318
   197
          lastToken = lastAdded
wenzelm@34318
   198
        else
wenzelm@34318
   199
          lastToken = beforeChange
wenzelm@34318
   200
      
wenzelm@34318
   201
      // insert new tokens into list
wenzelm@34318
   202
      if (firstAdded != null) {
wenzelm@34483
   203
        firstAdded.prev = beforeChange
wenzelm@34318
   204
        if (beforeChange != null)
wenzelm@34318
   205
          beforeChange.next = firstAdded
wenzelm@34318
   206
        else
wenzelm@34318
   207
          firstToken = firstAdded
wenzelm@34318
   208
      }
wenzelm@34318
   209
      else if (beforeChange != null)
wenzelm@34318
   210
        beforeChange.next = afterChange
wenzelm@34318
   211
      
wenzelm@34318
   212
      if (lastAdded != null) {
wenzelm@34318
   213
        lastAdded.next = afterChange
wenzelm@34318
   214
        if (afterChange != null)
wenzelm@34483
   215
          afterChange.prev = lastAdded
wenzelm@34318
   216
        else
wenzelm@34318
   217
          lastToken = lastAdded
wenzelm@34318
   218
      }
wenzelm@34318
   219
      else if (afterChange != null)
wenzelm@34483
   220
        afterChange.prev = beforeChange
wenzelm@34318
   221
    }
wenzelm@34318
   222
    
wenzelm@34485
   223
    token_changed(beforeChange, afterChange, firstRemoved)
wenzelm@34318
   224
  }
wenzelm@34318
   225
  
wenzelm@34485
   226
wenzelm@34318
   227
  
wenzelm@34485
   228
  /** command view **/
wenzelm@34485
   229
wenzelm@34485
   230
  val structural_changes = new EventBus[StructureChange]
wenzelm@34485
   231
wenzelm@34485
   232
  def commands = new Iterator[Command] {
wenzelm@34485
   233
    var current = firstToken
wenzelm@34485
   234
    def hasNext = current != null
wenzelm@34485
   235
    def next() = { val s = current.command ; current = s.last.next ; s }
wenzelm@34485
   236
  }
wenzelm@34485
   237
wenzelm@34485
   238
  def getContent(cmd: Command) = text.content(cmd.proper_start, cmd.proper_stop)
wenzelm@34485
   239
wenzelm@34485
   240
  def getNextCommandContaining(pos: Int): Command = {
wenzelm@34485
   241
    for (cmd <- commands) { if (pos < cmd.stop) return cmd }
wenzelm@34485
   242
    return null
wenzelm@34485
   243
  }
wenzelm@34485
   244
wenzelm@34485
   245
  private def token_changed(start: Token, stop: Token, removed: Token)
wenzelm@34485
   246
  {
wenzelm@34485
   247
    var removedCommands: List[Command] = Nil
wenzelm@34485
   248
    var first: Command = null
wenzelm@34485
   249
    var last: Command = null
wenzelm@34485
   250
wenzelm@34485
   251
    for(t <- tokens(removed)) {
wenzelm@34485
   252
      if (first == null)
wenzelm@34485
   253
        first = t.command
wenzelm@34485
   254
      if (t.command != last)
wenzelm@34485
   255
        removedCommands = t.command :: removedCommands
wenzelm@34485
   256
      last = t.command
wenzelm@34485
   257
    }
wenzelm@34485
   258
wenzelm@34485
   259
    var before: Command = null
wenzelm@34485
   260
    if (!removedCommands.isEmpty) {
wenzelm@34485
   261
      if (first.first == removed) {
wenzelm@34485
   262
        if (start == null)
wenzelm@34485
   263
          before = null
wenzelm@34485
   264
        else
wenzelm@34485
   265
          before = start.command
wenzelm@34485
   266
      }
wenzelm@34485
   267
      else
wenzelm@34485
   268
        before = first.prev
wenzelm@34485
   269
    }
wenzelm@34485
   270
wenzelm@34485
   271
    var addedCommands: List[Command] = Nil
wenzelm@34485
   272
    var scan: Token = null
wenzelm@34485
   273
    if (start != null) {
wenzelm@34485
   274
      val next = start.next
wenzelm@34485
   275
      if (first != null && first.first != removed) {
wenzelm@34485
   276
        scan = first.first
wenzelm@34485
   277
        if (before == null)
wenzelm@34485
   278
          before = first.prev
wenzelm@34485
   279
      }
wenzelm@34485
   280
      else if (next != null && next != stop) {
wenzelm@34485
   281
        if (next.kind == Token.Kind.COMMAND_START) {
wenzelm@34485
   282
          before = start.command
wenzelm@34485
   283
          scan = next
wenzelm@34485
   284
        }
wenzelm@34485
   285
        else if (first == null || first.first == removed) {
wenzelm@34485
   286
          first = start.command
wenzelm@34485
   287
          removedCommands = first :: removedCommands
wenzelm@34485
   288
          scan = first.first
wenzelm@34485
   289
          if (before == null)
wenzelm@34485
   290
            before = first.prev
wenzelm@34485
   291
        }
wenzelm@34485
   292
        else {
wenzelm@34485
   293
          scan = first.first
wenzelm@34485
   294
          if (before == null)
wenzelm@34485
   295
            before = first.prev
wenzelm@34485
   296
        }
wenzelm@34485
   297
      }
wenzelm@34485
   298
    }
wenzelm@34485
   299
    else
wenzelm@34485
   300
      scan = firstToken
wenzelm@34485
   301
wenzelm@34485
   302
    var stopScan: Token = null
wenzelm@34485
   303
    if (stop != null) {
wenzelm@34485
   304
      if (stop == stop.command.first)
wenzelm@34485
   305
        stopScan = stop
wenzelm@34485
   306
      else
wenzelm@34485
   307
        stopScan = stop.command.last.next
wenzelm@34485
   308
    }
wenzelm@34485
   309
    else if (last != null)
wenzelm@34485
   310
      stopScan = last.last.next
wenzelm@34485
   311
    else
wenzelm@34485
   312
      stopScan = null
wenzelm@34485
   313
wenzelm@34485
   314
    var cmdStart: Token = null
wenzelm@34485
   315
    var cmdStop: Token = null
wenzelm@34485
   316
    var overrun = false
wenzelm@34485
   317
    var finished = false
wenzelm@34485
   318
    while (scan != null && !finished) {
wenzelm@34485
   319
      if (scan == stopScan) {
wenzelm@34485
   320
        if (scan.kind == Token.Kind.COMMAND_START)
wenzelm@34485
   321
          finished = true
wenzelm@34485
   322
        else
wenzelm@34485
   323
          overrun = true
wenzelm@34485
   324
      }
wenzelm@34485
   325
wenzelm@34485
   326
      if (scan.kind == Token.Kind.COMMAND_START && cmdStart != null && !finished) {
wenzelm@34485
   327
        if (!overrun) {
wenzelm@34485
   328
          addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
wenzelm@34485
   329
          cmdStart = scan
wenzelm@34485
   330
          cmdStop = scan
wenzelm@34485
   331
        }
wenzelm@34485
   332
        else
wenzelm@34485
   333
          finished = true
wenzelm@34485
   334
      }
wenzelm@34485
   335
      else if (!finished) {
wenzelm@34485
   336
        if (cmdStart == null)
wenzelm@34485
   337
          cmdStart = scan
wenzelm@34485
   338
        cmdStop = scan
wenzelm@34485
   339
      }
wenzelm@34485
   340
      if (overrun && !finished) {
wenzelm@34485
   341
        if (scan.command != last)
wenzelm@34485
   342
          removedCommands = scan.command :: removedCommands
wenzelm@34485
   343
        last = scan.command
wenzelm@34485
   344
      }
wenzelm@34485
   345
wenzelm@34485
   346
      if (!finished)
wenzelm@34485
   347
        scan = scan.next
wenzelm@34485
   348
    }
wenzelm@34485
   349
wenzelm@34485
   350
    if (cmdStart != null)
wenzelm@34485
   351
      addedCommands = new Command(this, cmdStart, cmdStop) :: addedCommands
wenzelm@34485
   352
wenzelm@34485
   353
    // relink commands
wenzelm@34485
   354
    addedCommands = addedCommands.reverse
wenzelm@34485
   355
    removedCommands = removedCommands.reverse
wenzelm@34485
   356
wenzelm@34485
   357
    structural_changes.event(new StructureChange(before, addedCommands, removedCommands))
wenzelm@34485
   358
  }
wenzelm@34318
   359
}