--- a/src/Tools/jEdit/src/proofdocument/Token.scala Fri Jul 03 21:54:00 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala Sat Jul 04 14:14:07 2009 +0200
@@ -12,7 +12,8 @@
object Token {
- object Kind extends Enumeration {
+ object Kind extends Enumeration
+ {
val COMMAND_START = Value("COMMAND_START")
val COMMENT = Value("COMMENT")
val OTHER = Value("OTHER")
@@ -22,8 +23,8 @@
def stop(t: Token) = starts(t) + t.length
tokens match {
case Nil => ""
- case t :: tokens =>
- val (res, _) = tokens.foldLeft(t.content, stop(t))((a, token) =>
+ case tok :: toks =>
+ val (res, _) = toks.foldLeft(tok.content, stop(tok))((a, token) =>
(a._1 + " " * (starts(token) - a._2) + token.content, stop(token)))
res
}
@@ -31,9 +32,11 @@
}
-class Token(val content: String, val kind: Token.Kind.Value) {
- import Token.Kind._
+class Token(
+ val content: String,
+ val kind: Token.Kind.Value)
+{
+ override def toString = content
val length = content.length
- override def toString = content
- val is_start = kind == COMMAND_START || kind == COMMENT
+ val is_start = kind == Token.Kind.COMMAND_START || kind == Token.Kind.COMMENT
}