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