src/Tools/jEdit/src/proofdocument/ProofDocument.scala
changeset 34689 810bf0b27bcb
parent 34676 9e725d34df7b
child 34693 3e995f100ad2
     1.1 --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Aug 27 16:41:36 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Sep 01 13:49:25 2009 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4  import scala.collection.mutable.ListBuffer
     1.5  import java.util.regex.Pattern
     1.6  import isabelle.prover.{Prover, Command, Command_State}
     1.7 -import isabelle.utils.LinearSet
     1.8  
     1.9  
    1.10  object ProofDocument
    1.11 @@ -36,7 +35,7 @@
    1.12  
    1.13    val empty =
    1.14      new ProofDocument(isabelle.jedit.Isabelle.system.id(),
    1.15 -      LinearSet(), Map(), LinearSet(), Map(), _ => false,
    1.16 +      Linear_Set(), Map(), Linear_Set(), Map(), _ => false,
    1.17        actor(loop(react{case _ =>}))) // ignoring actor
    1.18  
    1.19    type StructureChange = List[(Option[Command], Option[Command])]
    1.20 @@ -45,9 +44,9 @@
    1.21  
    1.22  class ProofDocument(
    1.23    val id: String,
    1.24 -  val tokens: LinearSet[Token],
    1.25 +  val tokens: Linear_Set[Token],
    1.26    val token_start: Map[Token, Int],
    1.27 -  val commands: LinearSet[Command],
    1.28 +  val commands: Linear_Set[Command],
    1.29    var states: Map[Command, Command_State],
    1.30    is_command_keyword: String => Boolean,
    1.31    change_receiver: Actor)
    1.32 @@ -166,7 +165,7 @@
    1.33      new_token_start: Map[Token, Int]):
    1.34    (ProofDocument, StructureChange) =
    1.35    {
    1.36 -    val new_tokenset = (LinearSet() ++ new_tokens).asInstanceOf[LinearSet[Token]]
    1.37 +    val new_tokenset = Linear_Set[Token]() ++ new_tokens
    1.38      val cmd_before_change = before_change match {
    1.39        case None => None
    1.40        case Some(bc) =>