49 def contains(i: Offset): Boolean = start == i || start < i && i < stop |
49 def contains(i: Offset): Boolean = start == i || start < i && i < stop |
50 def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop |
50 def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop |
51 def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start) |
51 def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start) |
52 def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start |
52 def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start |
53 |
53 |
|
54 def apart(that: Range): Boolean = |
|
55 (this.start max that.start) > (this.stop min that.stop) |
|
56 |
54 def restrict(that: Range): Range = |
57 def restrict(that: Range): Range = |
55 Range(this.start max that.start, this.stop min that.stop) |
58 Range(this.start max that.start, this.stop min that.stop) |
56 |
59 |
57 def try_restrict(that: Range): Option[Range] = |
60 def try_restrict(that: Range): Option[Range] = |
58 try { Some (restrict(that)) } |
61 if (this apart that) None |
59 catch { case ERROR(_) => None } |
62 else Some(restrict(that)) |
|
63 |
|
64 def try_join(that: Range): Option[Range] = |
|
65 if (this apart that) None |
|
66 else Some(Range(this.start min that.start, this.stop max that.stop)) |
60 } |
67 } |
61 |
68 |
62 |
69 |
63 /* perspective */ |
70 /* perspective */ |
64 |
71 |
66 { |
73 { |
67 val empty: Perspective = Perspective(Nil) |
74 val empty: Perspective = Perspective(Nil) |
68 |
75 |
69 def apply(ranges: Seq[Range]): Perspective = |
76 def apply(ranges: Seq[Range]): Perspective = |
70 { |
77 { |
71 val sorted_ranges = ranges.toArray |
|
72 Sorting.quickSort(sorted_ranges)(Range.Ordering) |
|
73 |
|
74 val result = new mutable.ListBuffer[Text.Range] |
78 val result = new mutable.ListBuffer[Text.Range] |
75 var last: Option[Text.Range] = None |
79 var last: Option[Text.Range] = None |
76 for (range <- sorted_ranges) |
80 def ship(next: Option[Range]) { result ++= last; last = next } |
|
81 |
|
82 for (range <- ranges.sortBy(_.start)) |
77 { |
83 { |
78 last match { |
84 last match { |
79 case Some(last_range) |
85 case None => ship(Some(range)) |
80 if ((last_range overlaps range) || last_range.stop == range.start) => |
86 case Some(last_range) => |
81 last = Some(Text.Range(last_range.start, range.stop)) |
87 last_range.try_join(range) match { |
82 case _ => |
88 case None => ship(Some(range)) |
83 result ++= last |
89 case joined => last = joined |
84 last = Some(range) |
90 } |
85 } |
91 } |
86 } |
92 } |
87 result ++= last |
93 ship(None) |
88 new Perspective(result.toList) |
94 new Perspective(result.toList) |
89 } |
95 } |
90 } |
96 } |
91 |
97 |
92 sealed case class Perspective(ranges: List[Range]) // visible text partitioning in canonical order |
98 class Perspective private(val ranges: List[Range]) // visible text partitioning in canonical order |
93 { |
99 { |
94 def is_empty: Boolean = ranges.isEmpty |
100 def is_empty: Boolean = ranges.isEmpty |
95 def range: Range = |
101 def range: Range = |
96 if (is_empty) Range(0) |
102 if (is_empty) Range(0) |
97 else Range(ranges.head.start, ranges.last.stop) |
103 else Range(ranges.head.start, ranges.last.stop) |
|
104 override def toString = ranges.toString |
98 } |
105 } |
99 |
106 |
100 |
107 |
101 /* information associated with text range */ |
108 /* information associated with text range */ |
102 |
109 |