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