src/Tools/jEdit/src/proofdocument/Token.scala
author immler@in.tum.de
Mon Apr 20 12:17:15 2009 +0200 (2009-04-20)
changeset 34551 bd2b8fde9e25
parent 34539 5d88e0681d44
child 34554 7dc6c231da40
permissions -rw-r--r--
incomplete changes of immutable tokens and commands
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
immler@34526
    21
  private def fill(n: Int) = {
immler@34526
    22
    val blanks = new Array[Char](n)
immler@34526
    23
    for(i <- 0 to n - 1) blanks(i) = ' '
immler@34526
    24
    new String(blanks)
immler@34526
    25
  }
immler@34551
    26
  def string_from_tokens (tokens: List[Token], starts: Map[Token, Int]): String = {
immler@34551
    27
    def stop(t: Token) = starts(t) + t.length
immler@34526
    28
    tokens match {
immler@34526
    29
      case Nil => ""
immler@34551
    30
      case t::tokens => ( tokens.foldLeft
immler@34551
    31
          (t.content, stop(t))
immler@34551
    32
          ((a, token) => (a._1 + fill(starts(token) - a._2) + token.content, stop(token)))
immler@34526
    33
        )._1
immler@34389
    34
    }
immler@34389
    35
  }
immler@34526
    36
immler@34388
    37
}
immler@34388
    38
immler@34551
    39
class Token(val content: String, val kind: Token.Kind.Value) {
immler@34526
    40
  val length = content.length
immler@34526
    41
  override def toString = content + "(" + kind + ")"
wenzelm@34318
    42
}