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