# HG changeset patch
# User wenzelm
# Date 1251805765 -7200
# Node ID 810bf0b27bcbbf6c6b68c185d5178ea43f5efdbc
# Parent  1310dc269b4a64665c8ae0c613f2362dbdff9db4
use Linear_Set from Isabelle/Pure.jar;

diff -r 1310dc269b4a -r 810bf0b27bcb src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Aug 27 16:41:36 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Sep 01 13:49:25 2009 +0200
@@ -13,7 +13,6 @@
 import scala.collection.mutable.ListBuffer
 import java.util.regex.Pattern
 import isabelle.prover.{Prover, Command, Command_State}
-import isabelle.utils.LinearSet
 
 
 object ProofDocument
@@ -36,7 +35,7 @@
 
   val empty =
     new ProofDocument(isabelle.jedit.Isabelle.system.id(),
-      LinearSet(), Map(), LinearSet(), Map(), _ => false,
+      Linear_Set(), Map(), Linear_Set(), Map(), _ => false,
       actor(loop(react{case _ =>}))) // ignoring actor
 
   type StructureChange = List[(Option[Command], Option[Command])]
@@ -45,9 +44,9 @@
 
 class ProofDocument(
   val id: String,
-  val tokens: LinearSet[Token],
+  val tokens: Linear_Set[Token],
   val token_start: Map[Token, Int],
-  val commands: LinearSet[Command],
+  val commands: Linear_Set[Command],
   var states: Map[Command, Command_State],
   is_command_keyword: String => Boolean,
   change_receiver: Actor)
@@ -166,7 +165,7 @@
     new_token_start: Map[Token, Int]):
   (ProofDocument, StructureChange) =
   {
-    val new_tokenset = (LinearSet() ++ new_tokens).asInstanceOf[LinearSet[Token]]
+    val new_tokenset = Linear_Set[Token]() ++ new_tokens
     val cmd_before_change = before_change match {
       case None => None
       case Some(bc) =>
diff -r 1310dc269b4a -r 810bf0b27bcb src/Tools/jEdit/src/utils/LinearSet.scala
--- a/src/Tools/jEdit/src/utils/LinearSet.scala	Thu Aug 27 16:41:36 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,101 +0,0 @@
-/*  Title:      LinearSet.scala
-    Author:     Makarius
-
-Sets with canonical linear order, or immutable linked-lists.
-*/
-package isabelle.utils
-
-object LinearSet
-{
-  def empty[A]: LinearSet[A] = new LinearSet[A]
-  def apply[A](elems: A*): LinearSet[A] =
-    (empty[A] /: elems) ((s, elem) => s + elem)
-
-  class Duplicate(s: String) extends Exception(s)
-  class Undefined(s: String) extends Exception(s)
-
-  private def make[A](first: Option[A], last: Option[A], b: Map[A, A]): LinearSet[A] =
-    new LinearSet[A] {
-      override val first_elem = first
-      override val last_elem = last
-      override val body = b
-    }
-}
-
-class LinearSet[A] extends scala.collection.immutable.Set[A]
-{
-  /* representation */
-
-  val first_elem: Option[A] = None
-  val last_elem: Option[A] = None
-  val body: Map[A, A] = Map.empty
-
-
-  /* basic methods */
-
-  def next(elem: A) = body.get(elem)
-  def prev(elem: A) = body.find(_._2 == elem).map(_._1)
-  override def isEmpty: Boolean = !last_elem.isDefined
-  def size: Int = if (isEmpty) 0 else body.size + 1
-
-  def empty[B] = LinearSet.empty[B]
-
-  def contains(elem: A): Boolean =
-    !isEmpty && (last_elem.get == elem || body.isDefinedAt(elem))
-
-  private def _insert_after(hook: Option[A], elem: A): LinearSet[A] =
-    if (contains(elem)) throw new LinearSet.Duplicate(elem.toString)
-    else hook match {
-      case Some(hook) =>
-        if (!contains(hook)) throw new LinearSet.Undefined(hook.toString)
-        else if (body.isDefinedAt(hook))
-          LinearSet.make(first_elem, last_elem, body - hook + (hook -> elem) + (elem -> body(hook)))
-        else LinearSet.make(first_elem, Some(elem), body + (hook -> elem))
-      case None =>
-        if (isEmpty) LinearSet.make(Some(elem), Some(elem), Map.empty)
-        else LinearSet.make(Some(elem), last_elem, body + (elem -> first_elem.get))
-    }
-
-  def insert_after(hook: Option[A], elems: Seq[A]): LinearSet[A] =
-    elems.reverse.foldLeft (this) ((ls, elem) => ls._insert_after(hook, elem))
-
-  def +(elem: A): LinearSet[A] = _insert_after(last_elem, elem)
-
-  def delete_after(elem: Option[A]): LinearSet[A] =
-    elem match {
-      case Some(elem) =>
-        if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
-        else if (!body.isDefinedAt(elem)) throw new LinearSet.Undefined(null)
-        else if (body(elem) == last_elem.get) LinearSet.make(first_elem, Some(elem), body - elem)
-        else LinearSet.make(first_elem, last_elem, body - elem - body(elem) + (elem -> body(body(elem))))
-      case None =>
-        if (isEmpty) throw new LinearSet.Undefined(null)
-        else if (size == 1) empty
-        else LinearSet.make(Some(body(first_elem.get)), last_elem, body - first_elem.get)
-    }
-
-  def delete_between(from: Option[A], to: Option[A]): LinearSet[A] = {
-    if(!first_elem.isDefined) this
-    else {
-      val next = if (from == last_elem) None
-                 else if (from == None) first_elem
-                 else from.map(body(_))
-      if (next == to) this
-      else delete_after(from).delete_between(from, to)
-    }
-  }
-
-  def -(elem: A): LinearSet[A] =
-    if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
-    else delete_after(body find (p => p._2 == elem) map (p => p._1))
-
-  def elements = new Iterator[A] {
-    private var next_elem = first_elem
-    def hasNext = next_elem.isDefined
-    def next = {
-      val elem = next_elem.get
-      next_elem = if (body.isDefinedAt(elem)) Some(body(elem)) else None
-      elem
-    }
-  }
-}
\ No newline at end of file