src/Tools/jEdit/src/proofdocument/Token.scala
author immler@in.tum.de
Fri Nov 28 15:34:52 2008 +0100 (2008-11-28)
changeset 34389 e858aafb4809
parent 34388 23b8351ecbbe
child 34390 fe1afce19eb1
permissions -rw-r--r--
moved methods to object Token
wenzelm@34318
     1
package isabelle.proofdocument
wenzelm@34318
     2
immler@34388
     3
object Token {
immler@34388
     4
  object Kind {
immler@34388
     5
    val COMMAND_START = "COMMAND_START"
immler@34388
     6
    val COMMENT = "COMMENT"
immler@34388
     7
  }
immler@34389
     8
immler@34389
     9
  def checkStart(t : Token[_], P : (Int) => Boolean)
immler@34389
    10
    = t != null && P(t.start)
immler@34389
    11
immler@34389
    12
  def checkStop(t : Token[_], P : (Int) => Boolean)
immler@34389
    13
    = t != null && P(t.stop)
immler@34389
    14
immler@34389
    15
  def scan(s : Token[_], f : (Token[_]) => Boolean) : Token[_] = {
immler@34389
    16
    var current = s
immler@34389
    17
    while (current != null) {
immler@34389
    18
      val next = current.next
immler@34389
    19
      if (next == null || f(next))
immler@34389
    20
        return current
immler@34389
    21
      current = next
immler@34389
    22
    }
immler@34389
    23
    return null
immler@34389
    24
  }
immler@34389
    25
immler@34388
    26
}
immler@34388
    27
immler@34388
    28
class Token[C](var start : Int, var stop : Int, var kind : String) {
wenzelm@34318
    29
  var next : Token[C] = null
wenzelm@34318
    30
  var previous : Token[C] = null
wenzelm@34318
    31
  var command : C = null.asInstanceOf[C]
wenzelm@34318
    32
  
wenzelm@34318
    33
  def length = stop - start
wenzelm@34318
    34
wenzelm@34318
    35
  def shift(offset : Int, bottomClamp : Int) {
wenzelm@34318
    36
    start = bottomClamp max (start + offset)
wenzelm@34318
    37
    stop = bottomClamp max (stop + offset)
wenzelm@34318
    38
  }
wenzelm@34318
    39
  
wenzelm@34318
    40
  override def hashCode() : Int = (31 + start) * 31 + stop
wenzelm@34318
    41
wenzelm@34318
    42
  override def equals(obj : Any) : Boolean = {
wenzelm@34318
    43
    if (super.equals(obj))
wenzelm@34318
    44
      return true;
wenzelm@34318
    45
    
wenzelm@34318
    46
    if (null == obj)
wenzelm@34318
    47
      return false;
wenzelm@34318
    48
    
wenzelm@34318
    49
    obj match {
wenzelm@34318
    50
      case other: Token[_] => 
wenzelm@34318
    51
        (start == other.start) && (stop == other.stop)
wenzelm@34318
    52
      case other: Any => false  
wenzelm@34318
    53
    }
wenzelm@34318
    54
  }
wenzelm@34318
    55
}