# HG changeset patch
# User immler@in.tum.de
# Date 1227882892 -3600
# Node ID e858aafb4809f0a4038760755f57b96ab85a1f26
# Parent  23b8351ecbbe3182891dbf7ebc1d47d4b5b939cc
moved methods to object Token

diff -r 23b8351ecbbe -r e858aafb4809 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- 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
         
diff -r 23b8351ecbbe -r e858aafb4809 src/Tools/jEdit/src/proofdocument/Token.scala
--- 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) {