use Linear_Set from Isabelle/Pure.jar;
authorwenzelm
Tue Sep 01 13:49:25 2009 +0200 (2009-09-01)
changeset 34689810bf0b27bcb
parent 34688 1310dc269b4a
child 34690 e588fe99cd68
use Linear_Set from Isabelle/Pure.jar;
src/Tools/jEdit/src/proofdocument/ProofDocument.scala
src/Tools/jEdit/src/utils/LinearSet.scala
     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) =>
     2.1 --- a/src/Tools/jEdit/src/utils/LinearSet.scala	Thu Aug 27 16:41:36 2009 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,101 +0,0 @@
     2.4 -/*  Title:      LinearSet.scala
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Sets with canonical linear order, or immutable linked-lists.
     2.8 -*/
     2.9 -package isabelle.utils
    2.10 -
    2.11 -object LinearSet
    2.12 -{
    2.13 -  def empty[A]: LinearSet[A] = new LinearSet[A]
    2.14 -  def apply[A](elems: A*): LinearSet[A] =
    2.15 -    (empty[A] /: elems) ((s, elem) => s + elem)
    2.16 -
    2.17 -  class Duplicate(s: String) extends Exception(s)
    2.18 -  class Undefined(s: String) extends Exception(s)
    2.19 -
    2.20 -  private def make[A](first: Option[A], last: Option[A], b: Map[A, A]): LinearSet[A] =
    2.21 -    new LinearSet[A] {
    2.22 -      override val first_elem = first
    2.23 -      override val last_elem = last
    2.24 -      override val body = b
    2.25 -    }
    2.26 -}
    2.27 -
    2.28 -class LinearSet[A] extends scala.collection.immutable.Set[A]
    2.29 -{
    2.30 -  /* representation */
    2.31 -
    2.32 -  val first_elem: Option[A] = None
    2.33 -  val last_elem: Option[A] = None
    2.34 -  val body: Map[A, A] = Map.empty
    2.35 -
    2.36 -
    2.37 -  /* basic methods */
    2.38 -
    2.39 -  def next(elem: A) = body.get(elem)
    2.40 -  def prev(elem: A) = body.find(_._2 == elem).map(_._1)
    2.41 -  override def isEmpty: Boolean = !last_elem.isDefined
    2.42 -  def size: Int = if (isEmpty) 0 else body.size + 1
    2.43 -
    2.44 -  def empty[B] = LinearSet.empty[B]
    2.45 -
    2.46 -  def contains(elem: A): Boolean =
    2.47 -    !isEmpty && (last_elem.get == elem || body.isDefinedAt(elem))
    2.48 -
    2.49 -  private def _insert_after(hook: Option[A], elem: A): LinearSet[A] =
    2.50 -    if (contains(elem)) throw new LinearSet.Duplicate(elem.toString)
    2.51 -    else hook match {
    2.52 -      case Some(hook) =>
    2.53 -        if (!contains(hook)) throw new LinearSet.Undefined(hook.toString)
    2.54 -        else if (body.isDefinedAt(hook))
    2.55 -          LinearSet.make(first_elem, last_elem, body - hook + (hook -> elem) + (elem -> body(hook)))
    2.56 -        else LinearSet.make(first_elem, Some(elem), body + (hook -> elem))
    2.57 -      case None =>
    2.58 -        if (isEmpty) LinearSet.make(Some(elem), Some(elem), Map.empty)
    2.59 -        else LinearSet.make(Some(elem), last_elem, body + (elem -> first_elem.get))
    2.60 -    }
    2.61 -
    2.62 -  def insert_after(hook: Option[A], elems: Seq[A]): LinearSet[A] =
    2.63 -    elems.reverse.foldLeft (this) ((ls, elem) => ls._insert_after(hook, elem))
    2.64 -
    2.65 -  def +(elem: A): LinearSet[A] = _insert_after(last_elem, elem)
    2.66 -
    2.67 -  def delete_after(elem: Option[A]): LinearSet[A] =
    2.68 -    elem match {
    2.69 -      case Some(elem) =>
    2.70 -        if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
    2.71 -        else if (!body.isDefinedAt(elem)) throw new LinearSet.Undefined(null)
    2.72 -        else if (body(elem) == last_elem.get) LinearSet.make(first_elem, Some(elem), body - elem)
    2.73 -        else LinearSet.make(first_elem, last_elem, body - elem - body(elem) + (elem -> body(body(elem))))
    2.74 -      case None =>
    2.75 -        if (isEmpty) throw new LinearSet.Undefined(null)
    2.76 -        else if (size == 1) empty
    2.77 -        else LinearSet.make(Some(body(first_elem.get)), last_elem, body - first_elem.get)
    2.78 -    }
    2.79 -
    2.80 -  def delete_between(from: Option[A], to: Option[A]): LinearSet[A] = {
    2.81 -    if(!first_elem.isDefined) this
    2.82 -    else {
    2.83 -      val next = if (from == last_elem) None
    2.84 -                 else if (from == None) first_elem
    2.85 -                 else from.map(body(_))
    2.86 -      if (next == to) this
    2.87 -      else delete_after(from).delete_between(from, to)
    2.88 -    }
    2.89 -  }
    2.90 -
    2.91 -  def -(elem: A): LinearSet[A] =
    2.92 -    if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
    2.93 -    else delete_after(body find (p => p._2 == elem) map (p => p._1))
    2.94 -
    2.95 -  def elements = new Iterator[A] {
    2.96 -    private var next_elem = first_elem
    2.97 -    def hasNext = next_elem.isDefined
    2.98 -    def next = {
    2.99 -      val elem = next_elem.get
   2.100 -      next_elem = if (body.isDefinedAt(elem)) Some(body(elem)) else None
   2.101 -      elem
   2.102 -    }
   2.103 -  }
   2.104 -}
   2.105 \ No newline at end of file