alternative constructor for Range singularities;
authorwenzelm
Fri Aug 20 12:12:28 2010 +0200 (2010-08-20)
changeset 38568f117ba49a59c
parent 38567 b670faa807c9
child 38569 9d480f6a2589
alternative constructor for Range singularities;
src/Pure/General/position.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/text.scala
     1.1 --- a/src/Pure/General/position.scala	Fri Aug 20 11:57:43 2010 +0200
     1.2 +++ b/src/Pure/General/position.scala	Fri Aug 20 12:12:28 2010 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    def get_range(pos: T): Option[Text.Range] =
     1.5      (get_offset(pos), get_end_offset(pos)) match {
     1.6        case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
     1.7 -      case (Some(start), None) => Some(Text.Range(start, start))
     1.8 +      case (Some(start), None) => Some(Text.Range(start))
     1.9        case (_, _) => None
    1.10      }
    1.11  
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Fri Aug 20 11:57:43 2010 +0200
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Fri Aug 20 12:12:28 2010 +0200
     2.3 @@ -40,8 +40,8 @@
     2.4  
     2.5      def overlapping(range: Text.Range, branches: T): T =
     2.6      {
     2.7 -      val start = Node[Any](range.start_range, Nil)
     2.8 -      val stop = Node[Any](range.stop_range, Nil)
     2.9 +      val start = Node[Any](Text.Range(range.start), Nil)
    2.10 +      val stop = Node[Any](Text.Range(range.stop), Nil)
    2.11        branches.get(stop) match {
    2.12          case Some(end) if range overlaps end._1.range =>
    2.13            update(branches.range(start, stop), end)
     3.1 --- a/src/Pure/PIDE/text.scala	Fri Aug 20 11:57:43 2010 +0200
     3.2 +++ b/src/Pure/PIDE/text.scala	Fri Aug 20 12:12:28 2010 +0200
     3.3 @@ -17,6 +17,11 @@
     3.4  
     3.5    /* range -- with total quasi-ordering */
     3.6  
     3.7 +  object Range
     3.8 +  {
     3.9 +    def apply(start: Offset): Range = Range(start, start)
    3.10 +  }
    3.11 +
    3.12    sealed case class Range(val start: Offset, val stop: Offset)
    3.13    {
    3.14      // denotation: {start} Un {i. start < i & i < stop}
    3.15 @@ -31,9 +36,6 @@
    3.16      def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start)
    3.17      def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start
    3.18  
    3.19 -    def start_range: Range = Range(start, start)
    3.20 -    def stop_range: Range = Range(stop, stop)
    3.21 -
    3.22      def restrict(that: Range): Range =
    3.23        Range(this.start max that.start, this.stop min that.stop)
    3.24    }