# HG changeset patch
# User wenzelm
# Date 1232395470 -3600
# Node ID 0f4b34445f40b4c183e1b60866c41ab467ce4115
# Parent  660c639870a4cc0ad1a592fe1de313d24587698d
turned Token.Kind into Enumeration;

diff -r 660c639870a4 -r 0f4b34445f40 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Jan 19 20:33:26 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Jan 19 21:04:30 2009 +0100
@@ -96,11 +96,13 @@
     var position = 0 
     while(matcher.find(position) && ! finished) {
       position = matcher.end()
-			val kind = if(isStartKeyword(matcher.group())){
+			val kind = if(isStartKeyword(matcher.group())) {
         Token.Kind.COMMAND_START
-      } else if (matcher.end() - matcher.start() > 2 && matcher.group().substring(0, 2) == "(*"){
+      } else if (matcher.end() - matcher.start() > 2 && matcher.group().substring(0, 2) == "(*") {
         Token.Kind.COMMENT
-      } else {""}
+      } else {
+        Token.Kind.OTHER
+      }
       val newToken = new Token(matcher.start() + matchStart, matcher.end() + matchStart, kind)
 
       if (firstAdded == null)
diff -r 660c639870a4 -r 0f4b34445f40 src/Tools/jEdit/src/proofdocument/Token.scala
--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Mon Jan 19 20:33:26 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Mon Jan 19 21:04:30 2009 +0100
@@ -9,23 +9,24 @@
 import isabelle.prover.Command
 
 object Token {
-  object Kind {
-    val COMMAND_START = "COMMAND_START"
-    val COMMENT = "COMMENT"
+  object Kind extends Enumeration {
+    val COMMAND_START = Value("COMMAND_START")
+    val COMMENT = Value("COMMENT")
+    val OTHER = Value("OTHER")
   }
 
   def checkStart(t : Token, P : (Int) => Boolean)
-    = t != null && P(t.start)
+  = t != null && P(t.start)
 
   def checkStop(t : Token, P : (Int) => Boolean)
-    = t != null && P(t.stop)
+  = t != null && P(t.stop)
 
   def scan(s : Token, f : Token => Boolean) : Token = {
     var current = s
     while (current != null) {
       val next = current.next
       if (next == null || f(next))
-        return current
+      return current
       current = next
     }
     return null
@@ -33,7 +34,7 @@
 
 }
 
-class Token(var start : Int, var stop : Int, var kind : String) {
+class Token(var start : Int, var stop : Int, var kind : Token.Kind.Value) {
   var next : Token = null
   var previous : Token = null
   var command : Command = null
@@ -49,10 +50,10 @@
 
   override def equals(obj : Any) : Boolean = {
     if (super.equals(obj))
-      return true;
+    return true;
     
     if (null == obj)
-      return false;
+    return false;
     
     obj match {
       case other: Token =>