src/Tools/jEdit/src/proofdocument/ProofDocument.scala
author wenzelm
Mon Jan 19 21:38:50 2009 +0100 (2009-01-19 ago)
changeset 34483 0923926022d7
parent 34482 0f4b34445f40
child 34485 6475bfb4ff99
permissions -rw-r--r--
superficial tuning;
wenzelm@34407
     1
/*
wenzelm@34408
     2
 * Document as list of tokens
wenzelm@34407
     3
 *
wenzelm@34407
     4
 * @author Johannes Hölzl, TU Munich
wenzelm@34407
     5
 */
wenzelm@34407
     6
wenzelm@34318
     7
package isabelle.proofdocument
wenzelm@34318
     8
wenzelm@34483
     9
wenzelm@34318
    10
import java.util.regex.Pattern
wenzelm@34318
    11
wenzelm@34318
    12
wenzelm@34483
    13
object ProofDocument
wenzelm@34483
    14
{
wenzelm@34318
    15
  // Be carefully when changeing this regex. Not only must it handle the 
wenzelm@34318
    16
  // spurious end of a token but also:  
wenzelm@34318
    17
  // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
wenzelm@34318
    18
  // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
wenzelm@34318
    19
  
wenzelm@34483
    20
  val token_pattern = 
wenzelm@34318
    21
    Pattern.compile(
wenzelm@34318
    22
      "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
wenzelm@34318
    23
      "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
wenzelm@34318
    24
      "(\\?'?|')[A-Za-z_0-9.]*|" + 
wenzelm@34318
    25
      "[A-Za-z_0-9.]+|" + 
wenzelm@34318
    26
      "[!#$%&*+-/<=>?@^_|~]+|" +
wenzelm@34318
    27
      "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
wenzelm@34318
    28
      "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
wenzelm@34318
    29
      "[()\\[\\]{}:;]", Pattern.MULTILINE)
wenzelm@34318
    30
}
wenzelm@34318
    31
wenzelm@34483
    32
abstract class ProofDocument(text: Text)
wenzelm@34483
    33
{
wenzelm@34483
    34
  protected var firstToken: Token = null
wenzelm@34483
    35
  protected var lastToken: Token = null
wenzelm@34318
    36
  private var active = false 
wenzelm@34318
    37
  
wenzelm@34456
    38
  text.changes += (e => textChanged(e.start, e.added, e.removed))
wenzelm@34318
    39
	
wenzelm@34456
    40
  def activate() {
wenzelm@34456
    41
    if (!active) {
wenzelm@34318
    42
      active = true
wenzelm@34318
    43
      textChanged(0, text.length, 0)
wenzelm@34318
    44
    }
wenzelm@34456
    45
  }
wenzelm@34318
    46
  
wenzelm@34483
    47
  protected def tokens(start: Token, stop: Token) =
wenzelm@34483
    48
    new Iterator[Token] {
wenzelm@34318
    49
      var current = start
wenzelm@34483
    50
      def hasNext = current != stop && current != null
wenzelm@34318
    51
      def next() = { val save = current ; current = current.next ; save }
wenzelm@34318
    52
    }
wenzelm@34318
    53
  
wenzelm@34483
    54
  protected def tokens(start: Token): Iterator[Token] = 
wenzelm@34318
    55
    tokens(start, null)
wenzelm@34318
    56
  
wenzelm@34483
    57
  protected def tokens() : Iterator[Token] =
wenzelm@34318
    58
    tokens(firstToken, null)
wenzelm@34318
    59
wenzelm@34318
    60
  private def textChanged(start : Int, addedLen : Int, removedLen : Int) {
wenzelm@34483
    61
    val check_start = Token.check_start _
wenzelm@34483
    62
    val check_stop = Token.check_stop _
wenzelm@34481
    63
    val scan = Token.scan _
wenzelm@34318
    64
    if (active == false)
wenzelm@34318
    65
      return
wenzelm@34318
    66
        
wenzelm@34318
    67
    var beforeChange = 
wenzelm@34483
    68
      if (check_stop(firstToken, _ < start)) scan(firstToken, _.stop >= start)
wenzelm@34318
    69
      else null
wenzelm@34318
    70
    
wenzelm@34318
    71
    var firstRemoved = 
wenzelm@34318
    72
      if (beforeChange != null) beforeChange.next
wenzelm@34483
    73
      else if (check_start(firstToken, _ <= start + removedLen)) firstToken
wenzelm@34318
    74
      else null 
wenzelm@34318
    75
wenzelm@34318
    76
    var lastRemoved = scan(firstRemoved, _.start > start + removedLen)
wenzelm@34318
    77
wenzelm@34318
    78
    var shiftToken = 
wenzelm@34318
    79
      if (lastRemoved != null) lastRemoved
wenzelm@34483
    80
      else if (check_start(firstToken, _ > start)) firstToken
wenzelm@34318
    81
      else null
wenzelm@34318
    82
    
wenzelm@34318
    83
    while(shiftToken != null) {
wenzelm@34318
    84
      shiftToken.shift(addedLen - removedLen, start)
wenzelm@34318
    85
      shiftToken = shiftToken.next
wenzelm@34318
    86
    }
wenzelm@34318
    87
    
wenzelm@34318
    88
    // scan changed tokens until the end of the text or a matching token is
wenzelm@34318
    89
    // found which is beyond the changed area
wenzelm@34318
    90
    val matchStart = if (beforeChange == null) 0 else beforeChange.stop
wenzelm@34483
    91
    var firstAdded: Token = null
wenzelm@34483
    92
    var lastAdded: Token = null
wenzelm@34318
    93
wenzelm@34483
    94
    val matcher = ProofDocument.token_pattern.matcher(text.content(matchStart, text.length))
wenzelm@34318
    95
    var finished = false
wenzelm@34318
    96
    var position = 0 
wenzelm@34483
    97
    while (matcher.find(position) && ! finished) {
wenzelm@34318
    98
      position = matcher.end()
wenzelm@34482
    99
			val kind = if(isStartKeyword(matcher.group())) {
immler@34388
   100
        Token.Kind.COMMAND_START
wenzelm@34482
   101
      } else if (matcher.end() - matcher.start() > 2 && matcher.group().substring(0, 2) == "(*") {
immler@34388
   102
        Token.Kind.COMMENT
wenzelm@34482
   103
      } else {
wenzelm@34482
   104
        Token.Kind.OTHER
wenzelm@34482
   105
      }
wenzelm@34481
   106
      val newToken = new Token(matcher.start() + matchStart, matcher.end() + matchStart, kind)
wenzelm@34318
   107
wenzelm@34318
   108
      if (firstAdded == null)
wenzelm@34318
   109
        firstAdded = newToken
wenzelm@34318
   110
      else {
wenzelm@34483
   111
        newToken.prev = lastAdded
wenzelm@34318
   112
        lastAdded.next = newToken
wenzelm@34318
   113
      }
wenzelm@34318
   114
      lastAdded = newToken
wenzelm@34318
   115
      
wenzelm@34483
   116
      while (check_stop(lastRemoved, _ < newToken.stop) &&
wenzelm@34318
   117
              lastRemoved.next != null)	
wenzelm@34318
   118
        lastRemoved = lastRemoved.next
wenzelm@34318
   119
			
wenzelm@34318
   120
      if (newToken.stop >= start + addedLen && 
wenzelm@34483
   121
            check_stop(lastRemoved, _ == newToken.stop))
wenzelm@34318
   122
        finished = true
wenzelm@34318
   123
    }
wenzelm@34318
   124
wenzelm@34318
   125
    var afterChange = if (lastRemoved != null) lastRemoved.next else null
wenzelm@34318
   126
		
wenzelm@34318
   127
    // remove superflous first token-change
wenzelm@34318
   128
    if (firstAdded != null && firstAdded == firstRemoved && 
wenzelm@34318
   129
          firstAdded.stop < start) {
wenzelm@34318
   130
      beforeChange = firstRemoved
wenzelm@34318
   131
      if (lastRemoved == firstRemoved) {
wenzelm@34318
   132
        lastRemoved = null
wenzelm@34318
   133
        firstRemoved = null
wenzelm@34318
   134
      }
wenzelm@34318
   135
      else {
wenzelm@34318
   136
        firstRemoved = firstRemoved.next
wenzelm@34318
   137
        if (firstRemoved == null)
wenzelm@34318
   138
          System.err.println("ERROR")
wenzelm@34318
   139
        assert(firstRemoved != null)
wenzelm@34318
   140
      }
wenzelm@34318
   141
wenzelm@34318
   142
      if (lastAdded == firstAdded) {
wenzelm@34318
   143
        lastAdded = null
wenzelm@34318
   144
        firstAdded = null
wenzelm@34318
   145
      }
wenzelm@34318
   146
      if (firstAdded != null)
wenzelm@34318
   147
        firstAdded = firstAdded.next
wenzelm@34318
   148
    }
wenzelm@34318
   149
    
wenzelm@34318
   150
    // remove superflous last token-change
wenzelm@34318
   151
    if (lastAdded != null && lastAdded == lastRemoved &&
wenzelm@34318
   152
          lastAdded.start > start + addedLen) {
wenzelm@34318
   153
      afterChange = lastRemoved
wenzelm@34318
   154
      if (firstRemoved == lastRemoved) {
wenzelm@34318
   155
        firstRemoved = null
wenzelm@34318
   156
        lastRemoved = null
wenzelm@34318
   157
      }
wenzelm@34318
   158
      else {
wenzelm@34483
   159
        lastRemoved = lastRemoved.prev
wenzelm@34318
   160
        if (lastRemoved == null)
wenzelm@34318
   161
          System.err.println("ERROR")
wenzelm@34318
   162
        assert(lastRemoved != null)
wenzelm@34318
   163
      }
wenzelm@34318
   164
      
wenzelm@34318
   165
      if (lastAdded == firstAdded) {
wenzelm@34318
   166
        lastAdded = null
wenzelm@34318
   167
        firstAdded = null
wenzelm@34318
   168
      }
wenzelm@34318
   169
      else
wenzelm@34483
   170
        lastAdded = lastAdded.prev
wenzelm@34318
   171
    }
wenzelm@34318
   172
    
wenzelm@34318
   173
    if (firstRemoved == null && firstAdded == null)
wenzelm@34318
   174
      return
wenzelm@34318
   175
    
wenzelm@34318
   176
    if (firstToken == null) {
wenzelm@34318
   177
      firstToken = firstAdded
wenzelm@34318
   178
      lastToken = lastAdded
wenzelm@34318
   179
    }
wenzelm@34318
   180
    else {
wenzelm@34318
   181
      // cut removed tokens out of list
wenzelm@34318
   182
      if (firstRemoved != null)
wenzelm@34483
   183
        firstRemoved.prev = null
wenzelm@34318
   184
      if (lastRemoved != null)
wenzelm@34318
   185
        lastRemoved.next = null
wenzelm@34318
   186
      
wenzelm@34318
   187
      if (firstToken == firstRemoved)
wenzelm@34318
   188
        if (firstAdded != null)
wenzelm@34318
   189
          firstToken = firstAdded
wenzelm@34318
   190
        else
wenzelm@34318
   191
          firstToken = afterChange
wenzelm@34318
   192
      
wenzelm@34318
   193
      if (lastToken == lastRemoved)
wenzelm@34318
   194
        if (lastAdded != null)
wenzelm@34318
   195
          lastToken = lastAdded
wenzelm@34318
   196
        else
wenzelm@34318
   197
          lastToken = beforeChange
wenzelm@34318
   198
      
wenzelm@34318
   199
      // insert new tokens into list
wenzelm@34318
   200
      if (firstAdded != null) {
wenzelm@34483
   201
        firstAdded.prev = beforeChange
wenzelm@34318
   202
        if (beforeChange != null)
wenzelm@34318
   203
          beforeChange.next = firstAdded
wenzelm@34318
   204
        else
wenzelm@34318
   205
          firstToken = firstAdded
wenzelm@34318
   206
      }
wenzelm@34318
   207
      else if (beforeChange != null)
wenzelm@34318
   208
        beforeChange.next = afterChange
wenzelm@34318
   209
      
wenzelm@34318
   210
      if (lastAdded != null) {
wenzelm@34318
   211
        lastAdded.next = afterChange
wenzelm@34318
   212
        if (afterChange != null)
wenzelm@34483
   213
          afterChange.prev = lastAdded
wenzelm@34318
   214
        else
wenzelm@34318
   215
          lastToken = lastAdded
wenzelm@34318
   216
      }
wenzelm@34318
   217
      else if (afterChange != null)
wenzelm@34483
   218
        afterChange.prev = beforeChange
wenzelm@34318
   219
    }
wenzelm@34318
   220
    
wenzelm@34318
   221
    tokenChanged(beforeChange, afterChange, firstRemoved)
wenzelm@34318
   222
  }
wenzelm@34318
   223
  
wenzelm@34456
   224
  protected def isStartKeyword(str: String): Boolean
wenzelm@34318
   225
  
wenzelm@34481
   226
  protected def tokenChanged(start: Token, stop: Token, removed: Token) 
wenzelm@34318
   227
}