# HG changeset patch
# User wenzelm
# Date 1232486981 -3600
# Node ID 2268cbe29fca78f295cf3e1497f6eae6960d5568
# Parent  20e9d420dbbb943b38b89506648ec4751b740709
Token: plain val kind;

diff -r 20e9d420dbbb -r 2268cbe29fca src/Tools/jEdit/src/proofdocument/Token.scala
--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Tue Jan 20 20:32:04 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Tue Jan 20 22:29:41 2009 +0100
@@ -33,7 +33,7 @@
   }
 }
 
-class Token(var start: Int, var stop: Int, var kind: Token.Kind.Value)
+class Token(var start: Int, var stop: Int, val kind: Token.Kind.Value)
 {
   var next: Token = null
   var prev: Token = null