# HG changeset patch
# User wenzelm
# Date 1282299148 -7200
# Node ID f117ba49a59ca4f9fe7bf9b2db41267d95618ef4
# Parent  b670faa807c969be24e10e5d326e7ebbc72ee602
alternative constructor for Range singularities;

diff -r b670faa807c9 -r f117ba49a59c src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Fri Aug 20 11:57:43 2010 +0200
+++ b/src/Pure/General/position.scala	Fri Aug 20 12:12:28 2010 +0200
@@ -23,7 +23,7 @@
   def get_range(pos: T): Option[Text.Range] =
     (get_offset(pos), get_end_offset(pos)) match {
       case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
-      case (Some(start), None) => Some(Text.Range(start, start))
+      case (Some(start), None) => Some(Text.Range(start))
       case (_, _) => None
     }
 
diff -r b670faa807c9 -r f117ba49a59c src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Fri Aug 20 11:57:43 2010 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Aug 20 12:12:28 2010 +0200
@@ -40,8 +40,8 @@
 
     def overlapping(range: Text.Range, branches: T): T =
     {
-      val start = Node[Any](range.start_range, Nil)
-      val stop = Node[Any](range.stop_range, Nil)
+      val start = Node[Any](Text.Range(range.start), Nil)
+      val stop = Node[Any](Text.Range(range.stop), Nil)
       branches.get(stop) match {
         case Some(end) if range overlaps end._1.range =>
           update(branches.range(start, stop), end)
diff -r b670faa807c9 -r f117ba49a59c src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Fri Aug 20 11:57:43 2010 +0200
+++ b/src/Pure/PIDE/text.scala	Fri Aug 20 12:12:28 2010 +0200
@@ -17,6 +17,11 @@
 
   /* range -- with total quasi-ordering */
 
+  object Range
+  {
+    def apply(start: Offset): Range = Range(start, start)
+  }
+
   sealed case class Range(val start: Offset, val stop: Offset)
   {
     // denotation: {start} Un {i. start < i & i < stop}
@@ -31,9 +36,6 @@
     def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
     def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
 
-    def start_range: Range = Range(start, start)
-    def stop_range: Range = Range(stop, stop)
-
     def restrict(that: Range): Range =
       Range(this.start max that.start, this.stop min that.stop)
   }