# HG changeset patch
# User immler@in.tum.de
# Date 1227883900 -3600
# Node ID fe1afce19eb1d74f5e0efd3b5830cca1aa49f8c5
# Parent  e858aafb4809f0a4038760755f57b96ab85a1f26
Token-functions with type-parameters

diff -r e858aafb4809 -r fe1afce19eb1 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Fri Nov 28 15:34:52 2008 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Fri Nov 28 15:51:40 2008 +0100
@@ -54,7 +54,9 @@
     tokens(firstToken, null)
 
   private def textChanged(start : Int, addedLen : Int, removedLen : Int) {
-    import Token.{checkStart, scan, checkStop}
+    val checkStart = Token.checkStart[C] _
+    val checkStop = Token.checkStop[C] _
+    val scan = Token.scan[C] _
     if (active == false)
       return
         
diff -r e858aafb4809 -r fe1afce19eb1 src/Tools/jEdit/src/proofdocument/Token.scala
--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Fri Nov 28 15:34:52 2008 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Fri Nov 28 15:51:40 2008 +0100
@@ -6,13 +6,13 @@
     val COMMENT = "COMMENT"
   }
 
-  def checkStart(t : Token[_], P : (Int) => Boolean)
+  def checkStart[C](t : Token[C], P : (Int) => Boolean)
     = t != null && P(t.start)
 
-  def checkStop(t : Token[_], P : (Int) => Boolean)
+  def checkStop[C](t : Token[C], P : (Int) => Boolean)
     = t != null && P(t.stop)
 
-  def scan(s : Token[_], f : (Token[_]) => Boolean) : Token[_] = {
+  def scan[C](s : Token[C], f : (Token[C]) => Boolean) : Token[C] = {
     var current = s
     while (current != null) {
       val next = current.next
diff -r e858aafb4809 -r fe1afce19eb1 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Fri Nov 28 15:34:52 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Fri Nov 28 15:51:40 2008 +0100
@@ -6,7 +6,7 @@
 
 import javax.swing.SwingUtilities
 
-import isabelle.proofdocument.{ ProofDocument, Text }
+import isabelle.proofdocument.{ ProofDocument, Text, Token }
 import isabelle.IsabelleProcess.Result
 import isabelle.YXML.parse_failsafe
 import isabelle.XML.{ Elem, Tree }
@@ -106,12 +106,9 @@
               
       case IsabelleProcess.Kind.STATUS =>
         System.err.println("ST: " + tree)
-        val state = tree match { case Elem("message", _, 
+        val state = tree match { case Elem("message", _,
                                            Elem (name, _, _) :: _) => name
                                  case _ => null }
-/*        val markup_type =
-        val markup_begin =
-        val markup_end =*/
 
         if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE) {
           state match {