--- a/src/Tools/jEdit/src/proofdocument/Token.scala Fri Nov 28 15:00:07 2008 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala Fri Nov 28 15:34:52 2008 +0100
@@ -5,6 +5,24 @@
val COMMAND_START = "COMMAND_START"
val COMMENT = "COMMENT"
}
+
+ def checkStart(t : Token[_], P : (Int) => Boolean)
+ = t != null && P(t.start)
+
+ def checkStop(t : Token[_], P : (Int) => Boolean)
+ = 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
+ current = next
+ }
+ return null
+ }
+
}
class Token[C](var start : Int, var stop : Int, var kind : String) {