package isabelle.proofdocument

import java.util.regex.Pattern

import isabelle.utils.EventSource

object ProofDocument {

  // Be carefully when changeing this regex. Not only must it handle the 

  // spurious end of a token but also:  

  // Bug ID: 5050507 Pattern.matches throws StackOverflow Error

  // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507

  val tokenPattern = 

    Pattern.compile(

      "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +

      "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +

      "(\\?'?|')[A-Za-z_0-9.]*|" + 

      "[A-Za-z_0-9.]+|" + 

      "[!#$%&*+-/<=>?@^_|~]+|" +

      "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +

      "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +

      "[()\\[\\]{}:;]", Pattern.MULTILINE)

}

abstract class ProofDocument[C](text : Text) {

  import ProofDocument._

  protected var firstToken : Token[C] = null

  protected var lastToken : Token[C] = null

  private var active = false 

  {

    text.changes.add(e => textChanged(e.start, e.added, e.removed))

  }

  def activate() : Unit =

    if (! active) {

      active = true

      textChanged(0, text.length, 0)

    }

  protected def tokens(start : Token[C], stop : Token[C]) = 

    new Iterator[Token[C]]() {

      var current = start

      def hasNext() = current != stop && current != null

      def next() = { val save = current ; current = current.next ; save }

    }

  protected def tokens(start : Token[C]) : Iterator[Token[C]] = 

    tokens(start, null)

  protected def tokens() : Iterator[Token[C]] = 

    tokens(firstToken, null)

  private def checkStart(t : Token[C], P : (Int) => Boolean)

    = t != null && P(t.start)

  private def checkStop(t : Token[C], P : (Int) => Boolean)

    = t != null && P(t.stop)

  private def scan(s : Token[C], f : (Token[C]) => Boolean) : Token[C] = {

    var current = s

    while (current != null) {

      val next = current.next

      if (next == null || f(next))

        return current

      current = next

    }

    return null

  }

  private def textChanged(start : Int, addedLen : Int, removedLen : Int) {

    if (active == false)

      return

    var beforeChange = 

      if (checkStop(firstToken, _ < start)) scan(firstToken, _.stop >= start) 

      else null

    var firstRemoved = 

      if (beforeChange != null) beforeChange.next

      else if (checkStart(firstToken, _ <= start + removedLen)) firstToken

      else null 

    var lastRemoved = scan(firstRemoved, _.start > start + removedLen)

    var shiftToken = 

      if (lastRemoved != null) lastRemoved

      else if (checkStart(firstToken, _ > start)) firstToken

      else null

    while(shiftToken != null) {

      shiftToken.shift(addedLen - removedLen, start)

      shiftToken = shiftToken.next

    }

    // scan changed tokens until the end of the text or a matching token is

    // found which is beyond the changed area

    val matchStart = if (beforeChange == null) 0 else beforeChange.stop

    var firstAdded : Token[C] = null

    var lastAdded : Token[C] = null

    val matcher = tokenPattern.matcher(text.content(matchStart, text.length))

    var finished = false

    var position = 0 

    while(matcher.find(position) && ! finished) {

      position = matcher.end()

      val newToken = new Token[C](matcher.start() + matchStart, 

                                  matcher.end() + matchStart,

                                  isStartKeyword(matcher.group()),

                                  matcher.end() - matcher.start() > 2 &&

                                  matcher.group().substring(0, 2) == "(*")

      if (firstAdded == null)

        firstAdded = newToken

      else {

        newToken.previous = lastAdded

        lastAdded.next = newToken

      }

      lastAdded = newToken

      while(checkStop(lastRemoved, _ < newToken.stop) &&

              lastRemoved.next != null)	

        lastRemoved = lastRemoved.next

      if (newToken.stop >= start + addedLen && 

            checkStop(lastRemoved, _ == newToken.stop) )

        finished = true

    }

    var afterChange = if (lastRemoved != null) lastRemoved.next else null

    // remove superflous first token-change

    if (firstAdded != null && firstAdded == firstRemoved && 

          firstAdded.stop < start) {

      beforeChange = firstRemoved

      if (lastRemoved == firstRemoved) {

        lastRemoved = null

        firstRemoved = null

      }

      else {

        firstRemoved = firstRemoved.next

        if (firstRemoved == null)

          System.err.println("ERROR")

        assert(firstRemoved != null)

      }

      if (lastAdded == firstAdded) {

        lastAdded = null

        firstAdded = null

      }

      if (firstAdded != null)

        firstAdded = firstAdded.next

    }

    // remove superflous last token-change

    if (lastAdded != null && lastAdded == lastRemoved &&

          lastAdded.start > start + addedLen) {

      afterChange = lastRemoved

      if (firstRemoved == lastRemoved) {

        firstRemoved = null

        lastRemoved = null

      }

      else {

        lastRemoved = lastRemoved.previous

        if (lastRemoved == null)

          System.err.println("ERROR")

        assert(lastRemoved != null)

      }

      if (lastAdded == firstAdded) {

        lastAdded = null

        firstAdded = null

      }

      else

        lastAdded = lastAdded.previous

    }

    if (firstRemoved == null && firstAdded == null)

      return

    if (firstToken == null) {

      firstToken = firstAdded

      lastToken = lastAdded

    }

    else {

      // cut removed tokens out of list

      if (firstRemoved != null)

        firstRemoved.previous = null

      if (lastRemoved != null)

        lastRemoved.next = null

      if (firstToken == firstRemoved)

        if (firstAdded != null)

          firstToken = firstAdded

        else

          firstToken = afterChange

      if (lastToken == lastRemoved)

        if (lastAdded != null)

          lastToken = lastAdded

        else

          lastToken = beforeChange

      // insert new tokens into list

      if (firstAdded != null) {

        firstAdded.previous = beforeChange

        if (beforeChange != null)

          beforeChange.next = firstAdded

        else

          firstToken = firstAdded

      }

      else if (beforeChange != null)

        beforeChange.next = afterChange

      if (lastAdded != null) {

        lastAdded.next = afterChange

        if (afterChange != null)

          afterChange.previous = lastAdded

        else

          lastToken = lastAdded

      }

      else if (afterChange != null)

        afterChange.previous = beforeChange

    }

    tokenChanged(beforeChange, afterChange, firstRemoved)

  }

  protected def isStartKeyword(str : String) : Boolean;

  protected def tokenChanged(start : Token[C], stop : Token[C], 

                             removed : Token[C]) 

}