src/Tools/jEdit/src/proofdocument/Token.scala
author wenzelm
Tue Jun 02 21:44:16 2009 +0200 (2009-06-02)
changeset 34585 4c65620f5318
parent 34584 3457ef52de04
child 34597 a0c84b0edb9a
permissions -rw-r--r--
tuned;
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@34585
    21
  def string_from_tokens(tokens: List[Token], starts: Token => Int): String = {
immler@34551
    22
    def stop(t: Token) = starts(t) + t.length
immler@34526
    23
    tokens match {
immler@34526
    24
      case Nil => ""
wenzelm@34585
    25
      case t :: tokens =>
wenzelm@34585
    26
        val (res, _) = tokens.foldLeft(t.content, stop(t))((a, token) =>
wenzelm@34585
    27
          (a._1 + " " * (starts(token) - a._2) + token.content, stop(token)))
wenzelm@34585
    28
        res
immler@34389
    29
    }
immler@34389
    30
  }
immler@34526
    31
immler@34388
    32
}
immler@34388
    33
immler@34551
    34
class Token(val content: String, val kind: Token.Kind.Value) {
immler@34526
    35
  val length = content.length
immler@34554
    36
  override def toString = content
wenzelm@34318
    37
}