# HG changeset patch
# User wenzelm
# Date 1232393606 -3600
# Node ID 660c639870a4cc0ad1a592fe1de313d24587698d
# Parent  017fae24829f4ddec8152431d96d9cf073b9d81a
replaced type parameter C by Command (thanks to globally simultaneous scope);

diff -r 017fae24829f -r 660c639870a4 src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Jan 19 15:56:58 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Jan 19 20:33:26 2009 +0100
@@ -28,11 +28,11 @@
 
 }
 
-abstract class ProofDocument[C](text : Text) {
+abstract class ProofDocument(text : Text) {
   import ProofDocument._
   
-  protected var firstToken : Token[C] = null
-  protected var lastToken : Token[C] = null
+  protected var firstToken : Token = null
+  protected var lastToken : Token = null
   private var active = false 
   
   text.changes += (e => textChanged(e.start, e.added, e.removed))
@@ -44,23 +44,23 @@
     }
   }
   
-  protected def tokens(start : Token[C], stop : Token[C]) = 
-    new Iterator[Token[C]]() {
+  protected def tokens(start : Token, stop : Token) = 
+    new Iterator[Token]() {
       var current = start
       def hasNext() = current != stop && current != null
       def next() = { val save = current ; current = current.next ; save }
     }
   
-  protected def tokens(start : Token[C]) : Iterator[Token[C]] = 
+  protected def tokens(start : Token) : Iterator[Token] = 
     tokens(start, null)
   
-  protected def tokens() : Iterator[Token[C]] = 
+  protected def tokens() : Iterator[Token] = 
     tokens(firstToken, null)
 
   private def textChanged(start : Int, addedLen : Int, removedLen : Int) {
-    val checkStart = Token.checkStart[C] _
-    val checkStop = Token.checkStop[C] _
-    val scan = Token.scan[C] _
+    val checkStart = Token.checkStart _
+    val checkStop = Token.checkStop _
+    val scan = Token.scan _
     if (active == false)
       return
         
@@ -88,8 +88,8 @@
     // scan changed tokens until the end of the text or a matching token is
     // found which is beyond the changed area
     val matchStart = if (beforeChange == null) 0 else beforeChange.stop
-    var firstAdded : Token[C] = null
-    var lastAdded : Token[C] = null
+    var firstAdded : Token = null
+    var lastAdded : Token = null
 
     val matcher = tokenPattern.matcher(text.content(matchStart, text.length))
     var finished = false
@@ -101,10 +101,7 @@
       } else if (matcher.end() - matcher.start() > 2 && matcher.group().substring(0, 2) == "(*"){
         Token.Kind.COMMENT
       } else {""}
-      val newToken = new Token[C](matcher.start() + matchStart, 
-                                  matcher.end() + matchStart,
-                                  kind
-                                  )
+      val newToken = new Token(matcher.start() + matchStart, matcher.end() + matchStart, kind)
 
       if (firstAdded == null)
         firstAdded = newToken
@@ -224,6 +221,5 @@
   
   protected def isStartKeyword(str: String): Boolean
   
-  protected def tokenChanged(start : Token[C], stop : Token[C], 
-                             removed : Token[C]) 
+  protected def tokenChanged(start: Token, stop: Token, removed: Token) 
 }
diff -r 017fae24829f -r 660c639870a4 src/Tools/jEdit/src/proofdocument/Token.scala
--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Mon Jan 19 15:56:58 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Mon Jan 19 20:33:26 2009 +0100
@@ -6,6 +6,7 @@
  */
 
 package isabelle.proofdocument
+import isabelle.prover.Command
 
 object Token {
   object Kind {
@@ -13,13 +14,13 @@
     val COMMENT = "COMMENT"
   }
 
-  def checkStart[C](t : Token[C], P : (Int) => Boolean)
+  def checkStart(t : Token, P : (Int) => Boolean)
     = t != null && P(t.start)
 
-  def checkStop[C](t : Token[C], P : (Int) => Boolean)
+  def checkStop(t : Token, P : (Int) => Boolean)
     = t != null && P(t.stop)
 
-  def scan[C](s : Token[C], f : (Token[C]) => Boolean) : Token[C] = {
+  def scan(s : Token, f : Token => Boolean) : Token = {
     var current = s
     while (current != null) {
       val next = current.next
@@ -32,10 +33,10 @@
 
 }
 
-class Token[C](var start : Int, var stop : Int, var kind : String) {
-  var next : Token[C] = null
-  var previous : Token[C] = null
-  var command : C = null.asInstanceOf[C]
+class Token(var start : Int, var stop : Int, var kind : String) {
+  var next : Token = null
+  var previous : Token = null
+  var command : Command = null
   
   def length = stop - start
 
@@ -54,7 +55,7 @@
       return false;
     
     obj match {
-      case other: Token[_] => 
+      case other: Token => 
         (start == other.start) && (stop == other.stop)
       case other: Any => false  
     }
diff -r 017fae24829f -r 660c639870a4 src/Tools/jEdit/src/prover/Command.scala
--- a/src/Tools/jEdit/src/prover/Command.scala	Mon Jan 19 15:56:58 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Command.scala	Mon Jan 19 20:33:26 2009 +0100
@@ -29,7 +29,7 @@
 }
 
 
-class Command(val document: Document, val first: Token[Command], val last: Token[Command])
+class Command(val document: Document, val first: Token, val last: Token)
 {
   val id = Isabelle.plugin.id()
   
diff -r 017fae24829f -r 660c639870a4 src/Tools/jEdit/src/prover/Document.scala
--- a/src/Tools/jEdit/src/prover/Document.scala	Mon Jan 19 15:56:58 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Document.scala	Mon Jan 19 20:33:26 2009 +0100
@@ -16,7 +16,7 @@
 }
 
 
-class Document(text : Text, val prover : Prover) extends ProofDocument[Command](text)
+class Document(text : Text, val prover : Prover) extends ProofDocument(text)
 {
   val structural_changes = new EventBus[Document.StructureChange]
 
@@ -40,8 +40,8 @@
     return null
   }
 
-  override def tokenChanged(start : Token[Command], stop : Token[Command],
-                            removed : Token[Command]) {
+  override def tokenChanged(start : Token, stop : Token, removed : Token)
+  {
     var removedCommands : List[Command] = Nil
     var first : Command = null
     var last : Command = null
@@ -67,7 +67,7 @@
     }
 
     var addedCommands : List[Command] = Nil
-    var scan : Token[Command] = null
+    var scan : Token = null
     if (start != null) {
       val next = start.next
       if (first != null && first.first != removed) {
@@ -97,7 +97,7 @@
     else
       scan = firstToken
 
-    var stopScan : Token[Command] = null
+    var stopScan : Token = null
     if (stop != null) {
       if (stop == stop.command.first)
         stopScan = stop
@@ -109,8 +109,8 @@
     else
       stopScan = null
 
-    var cmdStart : Token[Command] = null
-    var cmdStop : Token[Command] = null
+    var cmdStart : Token = null
+    var cmdStop : Token = null
     var overrun = false
     var finished = false
     while (scan != null && !finished) {