src/Tools/jEdit/src/proofdocument/token.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
permissions -rw-r--r--
misc modernization of names;
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
immler@34388
    11
object Token {
wenzelm@34636
    12
  object Kind extends Enumeration
wenzelm@34636
    13
  {
wenzelm@34482
    14
    val COMMAND_START = Value("COMMAND_START")
wenzelm@34482
    15
    val COMMENT = Value("COMMENT")
wenzelm@34482
    16
    val OTHER = Value("OTHER")
immler@34388
    17
  }
immler@34389
    18
wenzelm@34585
    19
  def string_from_tokens(tokens: List[Token], starts: Token => Int): String = {
immler@34551
    20
    def stop(t: Token) = starts(t) + t.length
immler@34526
    21
    tokens match {
immler@34526
    22
      case Nil => ""
wenzelm@34636
    23
      case tok :: toks =>
wenzelm@34636
    24
        val (res, _) = toks.foldLeft(tok.content, stop(tok))((a, token) =>
wenzelm@34585
    25
          (a._1 + " " * (starts(token) - a._2) + token.content, stop(token)))
wenzelm@34585
    26
        res
immler@34389
    27
    }
immler@34389
    28
  }
immler@34526
    29
immler@34388
    30
}
immler@34388
    31
wenzelm@34636
    32
class Token(
wenzelm@34636
    33
  val content: String,
wenzelm@34636
    34
  val kind: Token.Kind.Value)
wenzelm@34636
    35
{
wenzelm@34636
    36
  override def toString = content
immler@34526
    37
  val length = content.length
wenzelm@34636
    38
  val is_start = kind == Token.Kind.COMMAND_START || kind == Token.Kind.COMMENT
wenzelm@34318
    39
}