--- 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
--- 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
--- 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 {