src/Tools/jEdit/src/proofdocument/ProofDocument.scala
changeset 34318 c13e168a8ae6
child 34388 23b8351ecbbe
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Sun Oct 19 16:51:55 2008 +0200
     1.3 @@ -0,0 +1,236 @@
     1.4 +package isabelle.proofdocument
     1.5 +
     1.6 +import java.util.regex.Pattern
     1.7 +
     1.8 +import isabelle.utils.EventSource
     1.9 +
    1.10 +object ProofDocument {
    1.11 +  // Be carefully when changeing this regex. Not only must it handle the 
    1.12 +  // spurious end of a token but also:  
    1.13 +  // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
    1.14 +  // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
    1.15 +  
    1.16 +  val tokenPattern = 
    1.17 +    Pattern.compile(
    1.18 +      "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
    1.19 +      "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
    1.20 +      "(\\?'?|')[A-Za-z_0-9.]*|" + 
    1.21 +      "[A-Za-z_0-9.]+|" + 
    1.22 +      "[!#$%&*+-/<=>?@^_|~]+|" +
    1.23 +      "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
    1.24 +      "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
    1.25 +      "[()\\[\\]{}:;]", Pattern.MULTILINE)
    1.26 +
    1.27 +}
    1.28 +
    1.29 +abstract class ProofDocument[C](text : Text) {
    1.30 +  import ProofDocument._
    1.31 +  
    1.32 +  protected var firstToken : Token[C] = null
    1.33 +  protected var lastToken : Token[C] = null
    1.34 +  private var active = false 
    1.35 +  
    1.36 +  {
    1.37 +    text.changes.add(e => textChanged(e.start, e.added, e.removed))
    1.38 +  }
    1.39 +	
    1.40 +  def activate() : Unit =
    1.41 +    if (! active) {
    1.42 +      active = true
    1.43 +      textChanged(0, text.length, 0)
    1.44 +    }
    1.45 +  
    1.46 +  protected def tokens(start : Token[C], stop : Token[C]) = 
    1.47 +    new Iterator[Token[C]]() {
    1.48 +      var current = start
    1.49 +      def hasNext() = current != stop && current != null
    1.50 +      def next() = { val save = current ; current = current.next ; save }
    1.51 +    }
    1.52 +  
    1.53 +  protected def tokens(start : Token[C]) : Iterator[Token[C]] = 
    1.54 +    tokens(start, null)
    1.55 +  
    1.56 +  protected def tokens() : Iterator[Token[C]] = 
    1.57 +    tokens(firstToken, null)
    1.58 +
    1.59 +  private def checkStart(t : Token[C], P : (Int) => Boolean)
    1.60 +    = t != null && P(t.start)
    1.61 +
    1.62 +  private def checkStop(t : Token[C], P : (Int) => Boolean)
    1.63 +    = t != null && P(t.stop)
    1.64 +  
    1.65 +  private def scan(s : Token[C], f : (Token[C]) => Boolean) : Token[C] = {
    1.66 +    var current = s
    1.67 +    while (current != null) {
    1.68 +      val next = current.next
    1.69 +      if (next == null || f(next))
    1.70 +        return current
    1.71 +      current = next
    1.72 +    }
    1.73 +    return null
    1.74 +  }
    1.75 +
    1.76 +  private def textChanged(start : Int, addedLen : Int, removedLen : Int) {
    1.77 +    if (active == false)
    1.78 +      return
    1.79 +        
    1.80 +    var beforeChange = 
    1.81 +      if (checkStop(firstToken, _ < start)) scan(firstToken, _.stop >= start) 
    1.82 +      else null
    1.83 +    
    1.84 +    var firstRemoved = 
    1.85 +      if (beforeChange != null) beforeChange.next
    1.86 +      else if (checkStart(firstToken, _ <= start + removedLen)) firstToken
    1.87 +      else null 
    1.88 +
    1.89 +    var lastRemoved = scan(firstRemoved, _.start > start + removedLen)
    1.90 +
    1.91 +    var shiftToken = 
    1.92 +      if (lastRemoved != null) lastRemoved
    1.93 +      else if (checkStart(firstToken, _ > start)) firstToken
    1.94 +      else null
    1.95 +    
    1.96 +    while(shiftToken != null) {
    1.97 +      shiftToken.shift(addedLen - removedLen, start)
    1.98 +      shiftToken = shiftToken.next
    1.99 +    }
   1.100 +    
   1.101 +    // scan changed tokens until the end of the text or a matching token is
   1.102 +    // found which is beyond the changed area
   1.103 +    val matchStart = if (beforeChange == null) 0 else beforeChange.stop
   1.104 +    var firstAdded : Token[C] = null
   1.105 +    var lastAdded : Token[C] = null
   1.106 +
   1.107 +    val matcher = tokenPattern.matcher(text.content(matchStart, text.length))
   1.108 +    var finished = false
   1.109 +    var position = 0 
   1.110 +    while(matcher.find(position) && ! finished) {
   1.111 +      position = matcher.end()
   1.112 +			
   1.113 +      val newToken = new Token[C](matcher.start() + matchStart, 
   1.114 +                                  matcher.end() + matchStart,
   1.115 +                                  isStartKeyword(matcher.group()),
   1.116 +                                  matcher.end() - matcher.start() > 2 &&
   1.117 +                                  matcher.group().substring(0, 2) == "(*")
   1.118 +
   1.119 +      if (firstAdded == null)
   1.120 +        firstAdded = newToken
   1.121 +      else {
   1.122 +        newToken.previous = lastAdded
   1.123 +        lastAdded.next = newToken
   1.124 +      }
   1.125 +      lastAdded = newToken
   1.126 +      
   1.127 +      while(checkStop(lastRemoved, _ < newToken.stop) &&
   1.128 +              lastRemoved.next != null)	
   1.129 +        lastRemoved = lastRemoved.next
   1.130 +			
   1.131 +      if (newToken.stop >= start + addedLen && 
   1.132 +            checkStop(lastRemoved, _ == newToken.stop) )
   1.133 +        finished = true
   1.134 +    }
   1.135 +
   1.136 +    var afterChange = if (lastRemoved != null) lastRemoved.next else null
   1.137 +		
   1.138 +    // remove superflous first token-change
   1.139 +    if (firstAdded != null && firstAdded == firstRemoved && 
   1.140 +          firstAdded.stop < start) {
   1.141 +      beforeChange = firstRemoved
   1.142 +      if (lastRemoved == firstRemoved) {
   1.143 +        lastRemoved = null
   1.144 +        firstRemoved = null
   1.145 +      }
   1.146 +      else {
   1.147 +        firstRemoved = firstRemoved.next
   1.148 +        if (firstRemoved == null)
   1.149 +          System.err.println("ERROR")
   1.150 +        assert(firstRemoved != null)
   1.151 +      }
   1.152 +
   1.153 +      if (lastAdded == firstAdded) {
   1.154 +        lastAdded = null
   1.155 +        firstAdded = null
   1.156 +      }
   1.157 +      if (firstAdded != null)
   1.158 +        firstAdded = firstAdded.next
   1.159 +    }
   1.160 +    
   1.161 +    // remove superflous last token-change
   1.162 +    if (lastAdded != null && lastAdded == lastRemoved &&
   1.163 +          lastAdded.start > start + addedLen) {
   1.164 +      afterChange = lastRemoved
   1.165 +      if (firstRemoved == lastRemoved) {
   1.166 +        firstRemoved = null
   1.167 +        lastRemoved = null
   1.168 +      }
   1.169 +      else {
   1.170 +        lastRemoved = lastRemoved.previous
   1.171 +        if (lastRemoved == null)
   1.172 +          System.err.println("ERROR")
   1.173 +        assert(lastRemoved != null)
   1.174 +      }
   1.175 +      
   1.176 +      if (lastAdded == firstAdded) {
   1.177 +        lastAdded = null
   1.178 +        firstAdded = null
   1.179 +      }
   1.180 +      else
   1.181 +        lastAdded = lastAdded.previous
   1.182 +    }
   1.183 +    
   1.184 +    if (firstRemoved == null && firstAdded == null)
   1.185 +      return
   1.186 +    
   1.187 +    if (firstToken == null) {
   1.188 +      firstToken = firstAdded
   1.189 +      lastToken = lastAdded
   1.190 +    }
   1.191 +    else {
   1.192 +      // cut removed tokens out of list
   1.193 +      if (firstRemoved != null)
   1.194 +        firstRemoved.previous = null
   1.195 +      if (lastRemoved != null)
   1.196 +        lastRemoved.next = null
   1.197 +      
   1.198 +      if (firstToken == firstRemoved)
   1.199 +        if (firstAdded != null)
   1.200 +          firstToken = firstAdded
   1.201 +        else
   1.202 +          firstToken = afterChange
   1.203 +      
   1.204 +      if (lastToken == lastRemoved)
   1.205 +        if (lastAdded != null)
   1.206 +          lastToken = lastAdded
   1.207 +        else
   1.208 +          lastToken = beforeChange
   1.209 +      
   1.210 +      // insert new tokens into list
   1.211 +      if (firstAdded != null) {
   1.212 +        firstAdded.previous = beforeChange
   1.213 +        if (beforeChange != null)
   1.214 +          beforeChange.next = firstAdded
   1.215 +        else
   1.216 +          firstToken = firstAdded
   1.217 +      }
   1.218 +      else if (beforeChange != null)
   1.219 +        beforeChange.next = afterChange
   1.220 +      
   1.221 +      if (lastAdded != null) {
   1.222 +        lastAdded.next = afterChange
   1.223 +        if (afterChange != null)
   1.224 +          afterChange.previous = lastAdded
   1.225 +        else
   1.226 +          lastToken = lastAdded
   1.227 +      }
   1.228 +      else if (afterChange != null)
   1.229 +        afterChange.previous = beforeChange
   1.230 +    }
   1.231 +    
   1.232 +    tokenChanged(beforeChange, afterChange, firstRemoved)
   1.233 +  }
   1.234 +  
   1.235 +  protected def isStartKeyword(str : String) : Boolean;
   1.236 +  
   1.237 +  protected def tokenChanged(start : Token[C], stop : Token[C], 
   1.238 +                             removed : Token[C]) 
   1.239 +}