author | wenzelm |
Sun, 12 Mar 2017 19:06:10 +0100 | |
changeset 65203 | 314246c6eeaa |
parent 65197 | 8fada74d82be |
child 65234 | 1d6e9048cb62 |
permissions | -rw-r--r-- |
64611 | 1 |
/* Title: Pure/PIDE/line.scala |
64605 | 2 |
Author: Makarius |
3 |
||
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
4 |
Line-oriented text documents, with some bias towards VSCode. |
64605 | 5 |
*/ |
6 |
||
64611 | 7 |
package isabelle |
64605 | 8 |
|
9 |
||
10 |
import scala.annotation.tailrec |
|
11 |
||
12 |
||
13 |
object Line |
|
14 |
{ |
|
64806 | 15 |
/* logical lines */ |
16 |
||
17 |
def normalize(text: String): String = |
|
18 |
if (text.contains('\r')) text.replace("\r\n", "\n") else text |
|
19 |
||
20 |
def logical_lines(text: String): List[String] = |
|
21 |
Library.split_lines(normalize(text)) |
|
22 |
||
23 |
||
64605 | 24 |
/* position */ |
25 |
||
26 |
object Position |
|
27 |
{ |
|
64650 | 28 |
val zero: Position = Position() |
64605 | 29 |
} |
30 |
||
64650 | 31 |
sealed case class Position(line: Int = 0, column: Int = 0) |
64605 | 32 |
{ |
33 |
def line1: Int = line + 1 |
|
34 |
def column1: Int = column + 1 |
|
35 |
def print: String = line1.toString + ":" + column1.toString |
|
36 |
||
37 |
def compare(that: Position): Int = |
|
38 |
line compare that.line match { |
|
39 |
case 0 => column compare that.column |
|
40 |
case i => i |
|
41 |
} |
|
42 |
||
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
43 |
def advance(text: String): Position = |
64617 | 44 |
if (text.isEmpty) this |
45 |
else { |
|
64806 | 46 |
val lines = logical_lines(text) |
64619 | 47 |
val l = line + lines.length - 1 |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
48 |
val c = (if (l == line) column else 0) + Library.trim_line(lines.last).length |
64619 | 49 |
Position(l, c) |
64605 | 50 |
} |
51 |
} |
|
52 |
||
53 |
||
54 |
/* range (right-open interval) */ |
|
55 |
||
64647 | 56 |
object Range |
57 |
{ |
|
64666 | 58 |
def apply(start: Position): Range = Range(start, start) |
59 |
val zero: Range = Range(Position.zero) |
|
64647 | 60 |
} |
61 |
||
64605 | 62 |
sealed case class Range(start: Position, stop: Position) |
63 |
{ |
|
64 |
if (start.compare(stop) > 0) |
|
65 |
error("Bad line range: " + start.print + ".." + stop.print) |
|
66 |
||
64647 | 67 |
def print: String = |
68 |
if (start == stop) start.print |
|
69 |
else start.print + ".." + stop.print |
|
64605 | 70 |
} |
71 |
||
72 |
||
64649 | 73 |
/* positions within document node */ |
74 |
||
64651 | 75 |
sealed case class Node_Position(name: String, pos: Position = Position.zero) |
64650 | 76 |
{ |
77 |
def line: Int = pos.line |
|
78 |
def column: Int = pos.column |
|
79 |
} |
|
80 |
||
64651 | 81 |
sealed case class Node_Range(name: String, range: Range = Range.zero) |
64650 | 82 |
{ |
83 |
def start: Position = range.start |
|
84 |
def stop: Position = range.stop |
|
85 |
} |
|
64649 | 86 |
|
87 |
||
64605 | 88 |
/* document with newline as separator (not terminator) */ |
89 |
||
90 |
object Document |
|
91 |
{ |
|
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
92 |
def apply(text: String): Document = |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
93 |
Document(logical_lines(text).map(s => Line(Library.trim_substring(s)))) |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
94 |
|
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
95 |
val empty: Document = apply("") |
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
96 |
|
65159 | 97 |
private def split(line_text: String): List[Line] = |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
98 |
if (line_text == "") List(Line.empty) else apply(line_text).lines |
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
99 |
|
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
100 |
private def chop(lines: List[Line]): (String, List[Line]) = |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
101 |
lines match { |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
102 |
case Nil => ("", Nil) |
65159 | 103 |
case line :: rest => (line.text, rest) |
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
104 |
} |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
105 |
|
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
106 |
private def length(lines: List[Line]): Int = |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
107 |
if (lines.isEmpty) 0 |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
108 |
else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1 |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
109 |
|
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
110 |
def text(lines: List[Line]): String = lines.mkString("", "\n", "") |
64605 | 111 |
} |
112 |
||
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
113 |
sealed case class Document(lines: List[Line]) |
64605 | 114 |
{ |
65197 | 115 |
lazy val text_length: Text.Offset = Document.length(lines) |
116 |
def text_range: Text.Range = Text.Range(0, text_length) |
|
117 |
||
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
118 |
lazy val text: String = Document.text(lines) |
64672 | 119 |
|
64877 | 120 |
def try_get_text(range: Text.Range): Option[String] = |
121 |
if (text_range.contains(range)) Some(text.substring(range.start, range.stop)) |
|
122 |
else None |
|
123 |
||
64821 | 124 |
override def toString: String = text |
64605 | 125 |
|
126 |
override def equals(that: Any): Boolean = |
|
127 |
that match { |
|
128 |
case other: Document => lines == other.lines |
|
129 |
case _ => false |
|
130 |
} |
|
131 |
override def hashCode(): Int = lines.hashCode |
|
132 |
||
64683
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64682
diff
changeset
|
133 |
def position(text_offset: Text.Offset): Position = |
64605 | 134 |
{ |
135 |
@tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position = |
|
136 |
{ |
|
137 |
lines_rest match { |
|
64650 | 138 |
case Nil => require(i == 0); Position(lines_count) |
64605 | 139 |
case line :: ls => |
140 |
val n = line.text.length |
|
64617 | 141 |
if (ls.isEmpty || i <= n) |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
142 |
Position(lines_count).advance(line.text.substring(n - i)) |
64605 | 143 |
else move(i - (n + 1), lines_count + 1, ls) |
144 |
} |
|
145 |
} |
|
64681
642b6105e6f4
clarified signature: explicit Length to avoid implicit mistakes;
wenzelm
parents:
64679
diff
changeset
|
146 |
move(text_offset, 0, lines) |
64605 | 147 |
} |
148 |
||
64683
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64682
diff
changeset
|
149 |
def range(text_range: Text.Range): Range = |
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64682
diff
changeset
|
150 |
Range(position(text_range.start), position(text_range.stop)) |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64672
diff
changeset
|
151 |
|
64683
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64682
diff
changeset
|
152 |
def offset(pos: Position): Option[Text.Offset] = |
64605 | 153 |
{ |
154 |
val l = pos.line |
|
155 |
val c = pos.column |
|
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
156 |
val n = lines.length |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
157 |
if (0 <= l && l < n) { |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
158 |
if (0 <= c && c <= lines(l).text.length) { |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
159 |
val line_offset = |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
160 |
(0 /: lines.iterator.take(l)) { case (n, line) => n + line.text.length + 1 } |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
161 |
Some(line_offset + c) |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
162 |
} |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
163 |
else None |
64605 | 164 |
} |
65197 | 165 |
else if (l == n && c == 0) Some(text_length) |
64605 | 166 |
else None |
167 |
} |
|
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
168 |
|
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
169 |
def change(remove: Range, insert: String): Option[(List[Text.Edit], Document)] = |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
170 |
{ |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
171 |
for { |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
172 |
edit_start <- offset(remove.start) |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
173 |
if remove.stop == remove.start || offset(remove.stop).isDefined |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
174 |
l1 = remove.start.line |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
175 |
l2 = remove.stop.line |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
176 |
if l1 <= l2 |
65159 | 177 |
(removed_text, new_lines) <- |
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
178 |
{ |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
179 |
val c1 = remove.start.column |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
180 |
val c2 = remove.stop.column |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
181 |
|
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
182 |
val (prefix, lines1) = lines.splitAt(l1) |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
183 |
val (s1, rest1) = Document.chop(lines1) |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
184 |
|
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
185 |
if (l1 == l2) { |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
186 |
if (0 <= c1 && c1 <= c2 && c2 <= s1.length) { |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
187 |
Some( |
65203 | 188 |
if (lines1.isEmpty) ("", prefix ::: Document.split(insert)) |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
189 |
else { |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
190 |
val removed_text = s1.substring(c1, c2) |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
191 |
val changed_text = s1.substring(0, c1) + insert + s1.substring(c2) |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
192 |
(removed_text, prefix ::: Document.split(changed_text) ::: rest1) |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
193 |
}) |
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
194 |
} |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
195 |
else None |
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
196 |
} |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
197 |
else { |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
198 |
val (middle, lines2) = rest1.splitAt(l2 - l1 - 1) |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
199 |
val (s2, rest2) = Document.chop(lines2) |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
200 |
if (0 <= c1 && c1 <= s1.length && 0 <= c2 && c2 <= s2.length) { |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
201 |
Some( |
65203 | 202 |
if (lines1.isEmpty) ("", prefix ::: Document.split(insert)) |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
203 |
else { |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
204 |
val r1 = s1.substring(c1) |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
205 |
val r2 = s2.substring(0, c2) |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
206 |
val removed_text = |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
207 |
if (lines2.isEmpty) Document.text(Line(r1) :: middle) |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
208 |
else Document.text(Line(r1) :: middle ::: List(Line(r2))) |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
209 |
val changed_text = s1.substring(0, c1) + insert + s2.substring(c2) |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
210 |
(removed_text, prefix ::: Document.split(changed_text) ::: rest2) |
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
211 |
}) |
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
212 |
} |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
213 |
else None |
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
214 |
} |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
215 |
} |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
216 |
} |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
217 |
yield |
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
218 |
(Text.Edit.removes(edit_start, removed_text) ::: Text.Edit.inserts(edit_start, insert), |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65159
diff
changeset
|
219 |
Document(new_lines)) |
65157
cd977a5bd928
clarified Document.offset: including final position;
wenzelm
parents:
64877
diff
changeset
|
220 |
} |
64605 | 221 |
} |
222 |
||
223 |
||
224 |
/* line text */ |
|
225 |
||
226 |
val empty: Line = new Line("") |
|
227 |
def apply(text: String): Line = if (text == "") empty else new Line(text) |
|
228 |
} |
|
229 |
||
230 |
final class Line private(val text: String) |
|
231 |
{ |
|
232 |
require(text.forall(c => c != '\r' && c != '\n')) |
|
233 |
||
234 |
override def equals(that: Any): Boolean = |
|
235 |
that match { |
|
236 |
case other: Line => text == other.text |
|
237 |
case _ => false |
|
238 |
} |
|
239 |
override def hashCode(): Int = text.hashCode |
|
240 |
override def toString: String = text |
|
241 |
} |