--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Fri Nov 28 15:00:07 2008 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Fri Nov 28 15:34:52 2008 +0100
@@ -53,24 +53,8 @@
protected def tokens() : Iterator[Token[C]] =
tokens(firstToken, null)
- private def checkStart(t : Token[C], P : (Int) => Boolean)
- = t != null && P(t.start)
-
- private def checkStop(t : Token[C], P : (Int) => Boolean)
- = t != null && P(t.stop)
-
- private def scan(s : Token[C], f : (Token[C]) => Boolean) : Token[C] = {
- var current = s
- while (current != null) {
- val next = current.next
- if (next == null || f(next))
- return current
- current = next
- }
- return null
- }
-
private def textChanged(start : Int, addedLen : Int, removedLen : Int) {
+ import Token.{checkStart, scan, checkStop}
if (active == false)
return
--- 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) {