src/Tools/jEdit/src/proofdocument/Token.scala
author wenzelm
Mon Jan 19 21:38:50 2009 +0100 (2009-01-19)
changeset 34483 0923926022d7
parent 34482 0f4b34445f40
child 34492 2268cbe29fca
permissions -rw-r--r--
superficial tuning;
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@34483
     9
wenzelm@34483
    10
wenzelm@34481
    11
import isabelle.prover.Command
wenzelm@34318
    12
wenzelm@34483
    13
immler@34388
    14
object Token {
wenzelm@34482
    15
  object Kind extends Enumeration {
wenzelm@34482
    16
    val COMMAND_START = Value("COMMAND_START")
wenzelm@34482
    17
    val COMMENT = Value("COMMENT")
wenzelm@34482
    18
    val OTHER = Value("OTHER")
immler@34388
    19
  }
immler@34389
    20
wenzelm@34483
    21
  def check_start(t: Token, P: Int => Boolean) = { t != null && P(t.start) }
wenzelm@34483
    22
  def check_stop(t: Token, P: Int => Boolean) = { t != null && P(t.stop) }
immler@34389
    23
wenzelm@34483
    24
  def scan(s: Token, f: Token => Boolean): Token =
wenzelm@34483
    25
  {
immler@34389
    26
    var current = s
immler@34389
    27
    while (current != null) {
immler@34389
    28
      val next = current.next
wenzelm@34483
    29
      if (next == null || f(next)) return current
immler@34389
    30
      current = next
immler@34389
    31
    }
immler@34389
    32
    return null
immler@34389
    33
  }
immler@34388
    34
}
immler@34388
    35
wenzelm@34483
    36
class Token(var start: Int, var stop: Int, var kind: Token.Kind.Value)
wenzelm@34483
    37
{
wenzelm@34483
    38
  var next: Token = null
wenzelm@34483
    39
  var prev: Token = null
wenzelm@34483
    40
  var command: Command = null
wenzelm@34318
    41
  
wenzelm@34318
    42
  def length = stop - start
wenzelm@34318
    43
wenzelm@34483
    44
  def shift(offset: Int, bottom_clamp: Int) {
wenzelm@34483
    45
    start = bottom_clamp max (start + offset)
wenzelm@34483
    46
    stop = bottom_clamp max (stop + offset)
wenzelm@34318
    47
  }
wenzelm@34318
    48
  
wenzelm@34483
    49
  override def hashCode: Int = (31 + start) * 31 + stop
wenzelm@34318
    50
wenzelm@34483
    51
  override def equals(obj: Any): Boolean =
wenzelm@34483
    52
  {
wenzelm@34483
    53
    if (super.equals(obj)) return true
wenzelm@34483
    54
    if (null == obj) return false
wenzelm@34318
    55
    obj match {
wenzelm@34483
    56
      case other: Token => (start == other.start) && (stop == other.stop)
wenzelm@34483
    57
      case other: Any => false
wenzelm@34318
    58
    }
wenzelm@34318
    59
  }
wenzelm@34318
    60
}