# HG changeset patch
# User wenzelm
# Date 1263203743 -3600
# Node ID a3d66403f9c92a89a8a5f8bfc6678f81b6e235ba
# Parent  d91c3fce478eb1909dedb04a70f0b3819589a621# Parent  b32c68328d24e26844a38a37bb999ae13643baf4
merged

diff -r d91c3fce478e -r a3d66403f9c9 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Sun Jan 10 18:14:29 2010 +0100
+++ b/src/Pure/General/linear_set.scala	Mon Jan 11 10:55:43 2010 +0100
@@ -118,18 +118,26 @@
   override def isEmpty: Boolean = !rep.first.isDefined
   def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
 
-  def elements = new Iterator[A] {
-    private var next_elem = rep.first
+  def contains(elem: A): Boolean =
+    !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
+
+  private def elements_from(start: Option[A]): Iterator[A] = new Iterator[A] {
+    private var next_elem = start
     def hasNext = next_elem.isDefined
-    def next = {
-      val elem = next_elem.get
-      next_elem = rep.nexts.get(elem)
-      elem
-    }
+    def next =
+      next_elem match {
+        case Some(elem) =>
+          next_elem = rep.nexts.get(elem)
+          elem
+        case None => throw new NoSuchElementException("next on empty iterator")
+      }
   }
 
-  def contains(elem: A): Boolean =
-    !isEmpty && (rep.last.get == elem || rep.nexts.isDefinedAt(elem))
+  def elements: Iterator[A] = elements_from(rep.first)
+
+  def elements(elem: A): Iterator[A] =
+    if (contains(elem)) elements_from(Some(elem))
+    else throw new Linear_Set.Undefined(elem.toString)
 
   def + (elem: A): Linear_Set[A] = insert_after(rep.last, elem)
 
diff -r d91c3fce478e -r a3d66403f9c9 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Sun Jan 10 18:14:29 2010 +0100
+++ b/src/Pure/General/scan.scala	Mon Jan 11 10:55:43 2010 +0100
@@ -108,6 +108,7 @@
     def ++ (elems: Iterator[String]): Lexicon = (this /: elems) ((s, elem) => s + elem)
 
 
+
     /** RegexParsers methods **/
 
     override val whiteSpace = "".r
diff -r d91c3fce478e -r a3d66403f9c9 src/Pure/Thy/text_edit.scala
--- a/src/Pure/Thy/text_edit.scala	Sun Jan 10 18:14:29 2010 +0100
+++ b/src/Pure/Thy/text_edit.scala	Mon Jan 11 10:55:43 2010 +0100
@@ -11,8 +11,10 @@
 sealed abstract class Text_Edit
 {
   val start: Int
+  def text: String
   def after(offset: Int): Int
   def before(offset: Int): Int
+  def can_edit(string_length: Int, shift: Int): Boolean
   def edit(string: String, shift: Int): (Option[Text_Edit], String)
 }
 
diff -r d91c3fce478e -r a3d66403f9c9 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sun Jan 10 18:14:29 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Jan 11 10:55:43 2010 +0100
@@ -7,7 +7,7 @@
 package isabelle
 
 
-class Thy_Syntax
+object Thy_Syntax
 {
   private val parser = new Outer_Parse.Parser
   {