src/Tools/jEdit/src/proofdocument/Token.scala
author wenzelm
Mon Jan 19 21:04:30 2009 +0100 (2009-01-19)
changeset 34482 0f4b34445f40
parent 34481 660c639870a4
child 34483 0923926022d7
permissions -rw-r--r--
turned Token.Kind into Enumeration;
wenzelm@34407
     1
/*
wenzelm@34407
     2
 * Document tokens as text ranges
wenzelm@34407
     3
 *
wenzelm@34407
     4
 * @author Johannes Hölzl, TU Munich
wenzelm@34407
     5
 * @author Fabian Immler, TU Munich
wenzelm@34407
     6
 */
wenzelm@34407
     7
wenzelm@34318
     8
package isabelle.proofdocument
wenzelm@34481
     9
import isabelle.prover.Command
wenzelm@34318
    10
immler@34388
    11
object Token {
wenzelm@34482
    12
  object Kind extends Enumeration {
wenzelm@34482
    13
    val COMMAND_START = Value("COMMAND_START")
wenzelm@34482
    14
    val COMMENT = Value("COMMENT")
wenzelm@34482
    15
    val OTHER = Value("OTHER")
immler@34388
    16
  }
immler@34389
    17
wenzelm@34481
    18
  def checkStart(t : Token, P : (Int) => Boolean)
wenzelm@34482
    19
  = t != null && P(t.start)
immler@34389
    20
wenzelm@34481
    21
  def checkStop(t : Token, P : (Int) => Boolean)
wenzelm@34482
    22
  = t != null && P(t.stop)
immler@34389
    23
wenzelm@34481
    24
  def scan(s : Token, f : Token => Boolean) : Token = {
immler@34389
    25
    var current = s
immler@34389
    26
    while (current != null) {
immler@34389
    27
      val next = current.next
immler@34389
    28
      if (next == null || f(next))
wenzelm@34482
    29
      return current
immler@34389
    30
      current = next
immler@34389
    31
    }
immler@34389
    32
    return null
immler@34389
    33
  }
immler@34389
    34
immler@34388
    35
}
immler@34388
    36
wenzelm@34482
    37
class Token(var start : Int, var stop : Int, var kind : Token.Kind.Value) {
wenzelm@34481
    38
  var next : Token = null
wenzelm@34481
    39
  var previous : Token = null
wenzelm@34481
    40
  var command : Command = null
wenzelm@34318
    41
  
wenzelm@34318
    42
  def length = stop - start
wenzelm@34318
    43
wenzelm@34318
    44
  def shift(offset : Int, bottomClamp : Int) {
wenzelm@34318
    45
    start = bottomClamp max (start + offset)
wenzelm@34318
    46
    stop = bottomClamp max (stop + offset)
wenzelm@34318
    47
  }
wenzelm@34318
    48
  
wenzelm@34318
    49
  override def hashCode() : Int = (31 + start) * 31 + stop
wenzelm@34318
    50
wenzelm@34318
    51
  override def equals(obj : Any) : Boolean = {
wenzelm@34318
    52
    if (super.equals(obj))
wenzelm@34482
    53
    return true;
wenzelm@34318
    54
    
wenzelm@34318
    55
    if (null == obj)
wenzelm@34482
    56
    return false;
wenzelm@34318
    57
    
wenzelm@34318
    58
    obj match {
wenzelm@34481
    59
      case other: Token => 
wenzelm@34318
    60
        (start == other.start) && (stop == other.stop)
wenzelm@34318
    61
      case other: Any => false  
wenzelm@34318
    62
    }
wenzelm@34318
    63
  }
wenzelm@34318
    64
}