21 split_lines(normalize(text)) |
20 split_lines(normalize(text)) |
22 |
21 |
23 |
22 |
24 /* position */ |
23 /* position */ |
25 |
24 |
26 object Position |
25 object Position { |
27 { |
|
28 val zero: Position = Position() |
26 val zero: Position = Position() |
29 val offside: Position = Position(line = -1) |
27 val offside: Position = Position(line = -1) |
30 |
28 |
31 object Ordering extends scala.math.Ordering[Position] |
29 object Ordering extends scala.math.Ordering[Position] { |
32 { |
|
33 def compare(p1: Position, p2: Position): Int = p1 compare p2 |
30 def compare(p1: Position, p2: Position): Int = p1 compare p2 |
34 } |
31 } |
35 } |
32 } |
36 |
33 |
37 sealed case class Position(line: Int = 0, column: Int = 0) |
34 sealed case class Position(line: Int = 0, column: Int = 0) { |
38 { |
|
39 def line1: Int = line + 1 |
35 def line1: Int = line + 1 |
40 def column1: Int = column + 1 |
36 def column1: Int = column + 1 |
41 def print: String = line1.toString + ":" + column1.toString |
37 def print: String = line1.toString + ":" + column1.toString |
42 |
38 |
43 def compare(that: Position): Int = |
39 def compare(that: Position): Int = |
57 } |
53 } |
58 |
54 |
59 |
55 |
60 /* range (right-open interval) */ |
56 /* range (right-open interval) */ |
61 |
57 |
62 object Range |
58 object Range { |
63 { |
|
64 def apply(start: Position): Range = Range(start, start) |
59 def apply(start: Position): Range = Range(start, start) |
65 val zero: Range = Range(Position.zero) |
60 val zero: Range = Range(Position.zero) |
66 } |
61 } |
67 |
62 |
68 sealed case class Range(start: Position, stop: Position) |
63 sealed case class Range(start: Position, stop: Position) { |
69 { |
|
70 if (start.compare(stop) > 0) |
64 if (start.compare(stop) > 0) |
71 error("Bad line range: " + start.print + ".." + stop.print) |
65 error("Bad line range: " + start.print + ".." + stop.print) |
72 |
66 |
73 def print: String = |
67 def print: String = |
74 if (start == stop) start.print |
68 if (start == stop) start.print |
76 } |
70 } |
77 |
71 |
78 |
72 |
79 /* positions within document node */ |
73 /* positions within document node */ |
80 |
74 |
81 object Node_Position |
75 object Node_Position { |
82 { |
|
83 def offside(name: String): Node_Position = Node_Position(name, Position.offside) |
76 def offside(name: String): Node_Position = Node_Position(name, Position.offside) |
84 } |
77 } |
85 |
78 |
86 sealed case class Node_Position(name: String, pos: Position = Position.zero) |
79 sealed case class Node_Position(name: String, pos: Position = Position.zero) { |
87 { |
|
88 def line: Int = pos.line |
80 def line: Int = pos.line |
89 def line1: Int = pos.line1 |
81 def line1: Int = pos.line1 |
90 def column: Int = pos.column |
82 def column: Int = pos.column |
91 def column1: Int = pos.column1 |
83 def column1: Int = pos.column1 |
92 } |
84 } |
93 |
85 |
94 sealed case class Node_Range(name: String, range: Range = Range.zero) |
86 sealed case class Node_Range(name: String, range: Range = Range.zero) { |
95 { |
|
96 def start: Position = range.start |
87 def start: Position = range.start |
97 def stop: Position = range.stop |
88 def stop: Position = range.stop |
98 } |
89 } |
99 |
90 |
100 |
91 |
101 /* document with newline as separator (not terminator) */ |
92 /* document with newline as separator (not terminator) */ |
102 |
93 |
103 object Document |
94 object Document { |
104 { |
|
105 def apply(text: String): Document = |
95 def apply(text: String): Document = |
106 Document(logical_lines(text).map(s => Line(Library.isolate_substring(s)))) |
96 Document(logical_lines(text).map(s => Line(Library.isolate_substring(s)))) |
107 |
97 |
108 val empty: Document = apply("") |
98 val empty: Document = apply("") |
109 |
99 |
121 else (lines.foldLeft(0) { case (n, line) => n + line.text.length + 1 }) - 1 |
111 else (lines.foldLeft(0) { case (n, line) => n + line.text.length + 1 }) - 1 |
122 |
112 |
123 def text(lines: List[Line]): String = lines.mkString("", "\n", "") |
113 def text(lines: List[Line]): String = lines.mkString("", "\n", "") |
124 } |
114 } |
125 |
115 |
126 sealed case class Document(lines: List[Line]) |
116 sealed case class Document(lines: List[Line]) { |
127 { |
|
128 lazy val text_length: Text.Offset = Document.length(lines) |
117 lazy val text_length: Text.Offset = Document.length(lines) |
129 def text_range: Text.Range = Text.Range(0, text_length) |
118 def text_range: Text.Range = Text.Range(0, text_length) |
130 |
119 |
131 lazy val text: String = Document.text(lines) |
120 lazy val text: String = Document.text(lines) |
132 |
121 |
140 case other: Document => lines == other.lines |
129 case other: Document => lines == other.lines |
141 case _ => false |
130 case _ => false |
142 } |
131 } |
143 override def hashCode(): Int = lines.hashCode |
132 override def hashCode(): Int = lines.hashCode |
144 |
133 |
145 def position(text_offset: Text.Offset): Position = |
134 def position(text_offset: Text.Offset): Position = { |
146 { |
135 @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position = { |
147 @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position = |
|
148 { |
|
149 lines_rest match { |
136 lines_rest match { |
150 case Nil => require(i == 0, "bad Line.position.move"); Position(lines_count) |
137 case Nil => require(i == 0, "bad Line.position.move"); Position(lines_count) |
151 case line :: ls => |
138 case line :: ls => |
152 val n = line.text.length |
139 val n = line.text.length |
153 if (ls.isEmpty || i <= n) |
140 if (ls.isEmpty || i <= n) |
159 } |
146 } |
160 |
147 |
161 def range(text_range: Text.Range): Range = |
148 def range(text_range: Text.Range): Range = |
162 Range(position(text_range.start), position(text_range.stop)) |
149 Range(position(text_range.start), position(text_range.stop)) |
163 |
150 |
164 def offset(pos: Position): Option[Text.Offset] = |
151 def offset(pos: Position): Option[Text.Offset] = { |
165 { |
|
166 val l = pos.line |
152 val l = pos.line |
167 val c = pos.column |
153 val c = pos.column |
168 val n = lines.length |
154 val n = lines.length |
169 if (0 <= l && l < n) { |
155 if (0 <= l && l < n) { |
170 if (0 <= c && c <= lines(l).text.length) { |
156 if (0 <= c && c <= lines(l).text.length) { |
176 } |
162 } |
177 else if (l == n && c == 0) Some(text_length) |
163 else if (l == n && c == 0) Some(text_length) |
178 else None |
164 else None |
179 } |
165 } |
180 |
166 |
181 def change(remove: Range, insert: String): Option[(List[Text.Edit], Document)] = |
167 def change(remove: Range, insert: String): Option[(List[Text.Edit], Document)] = { |
182 { |
|
183 for { |
168 for { |
184 edit_start <- offset(remove.start) |
169 edit_start <- offset(remove.start) |
185 if remove.stop == remove.start || offset(remove.stop).isDefined |
170 if remove.stop == remove.start || offset(remove.stop).isDefined |
186 l1 = remove.start.line |
171 l1 = remove.start.line |
187 l2 = remove.stop.line |
172 l2 = remove.stop.line |
188 if l1 <= l2 |
173 if l1 <= l2 |
189 (removed_text, new_lines) <- |
174 (removed_text, new_lines) <- { |
190 { |
|
191 val c1 = remove.start.column |
175 val c1 = remove.start.column |
192 val c2 = remove.stop.column |
176 val c2 = remove.stop.column |
193 |
177 |
194 val (prefix, lines1) = lines.splitAt(l1) |
178 val (prefix, lines1) = lines.splitAt(l1) |
195 val (s1, rest1) = Document.chop(lines1) |
179 val (s1, rest1) = Document.chop(lines1) |
237 |
221 |
238 val empty: Line = new Line("") |
222 val empty: Line = new Line("") |
239 def apply(text: String): Line = if (text == "") empty else new Line(text) |
223 def apply(text: String): Line = if (text == "") empty else new Line(text) |
240 } |
224 } |
241 |
225 |
242 final class Line private(val text: String) |
226 final class Line private(val text: String) { |
243 { |
|
244 require(text.forall(c => c != '\r' && c != '\n'), "bad line text") |
227 require(text.forall(c => c != '\r' && c != '\n'), "bad line text") |
245 |
228 |
246 override def equals(that: Any): Boolean = |
229 override def equals(that: Any): Boolean = |
247 that match { |
230 that match { |
248 case other: Line => text == other.text |
231 case other: Line => text == other.text |