author | wenzelm |
Wed, 28 Dec 2016 17:10:09 +0100 | |
changeset 64682 | 7e119f32276a |
parent 64681 | 642b6105e6f4 |
child 64683 | c0c09b6dfbe0 |
permissions | -rw-r--r-- |
64611 | 1 |
/* Title: Pure/PIDE/line.scala |
64605 | 2 |
Author: Makarius |
3 |
||
4 |
Line-oriented text. |
|
5 |
*/ |
|
6 |
||
64611 | 7 |
package isabelle |
64605 | 8 |
|
9 |
||
10 |
import scala.annotation.tailrec |
|
11 |
||
12 |
||
13 |
object Line |
|
14 |
{ |
|
15 |
/* position */ |
|
16 |
||
17 |
object Position |
|
18 |
{ |
|
64650 | 19 |
val zero: Position = Position() |
64605 | 20 |
} |
21 |
||
64650 | 22 |
sealed case class Position(line: Int = 0, column: Int = 0) |
64605 | 23 |
{ |
24 |
def line1: Int = line + 1 |
|
25 |
def column1: Int = column + 1 |
|
26 |
def print: String = line1.toString + ":" + column1.toString |
|
27 |
||
28 |
def compare(that: Position): Int = |
|
29 |
line compare that.line match { |
|
30 |
case 0 => column compare that.column |
|
31 |
case i => i |
|
32 |
} |
|
33 |
||
64682 | 34 |
def advance(text: String, text_length: Text.Length): Position = |
64617 | 35 |
if (text.isEmpty) this |
36 |
else { |
|
37 |
val lines = Library.split_lines(text) |
|
64619 | 38 |
val l = line + lines.length - 1 |
64681
642b6105e6f4
clarified signature: explicit Length to avoid implicit mistakes;
wenzelm
parents:
64679
diff
changeset
|
39 |
val c = (if (l == line) column else 0) + text_length(Library.trim_line(lines.last)) |
64619 | 40 |
Position(l, c) |
64605 | 41 |
} |
42 |
} |
|
43 |
||
44 |
||
45 |
/* range (right-open interval) */ |
|
46 |
||
64647 | 47 |
object Range |
48 |
{ |
|
64666 | 49 |
def apply(start: Position): Range = Range(start, start) |
50 |
val zero: Range = Range(Position.zero) |
|
64647 | 51 |
} |
52 |
||
64605 | 53 |
sealed case class Range(start: Position, stop: Position) |
54 |
{ |
|
55 |
if (start.compare(stop) > 0) |
|
56 |
error("Bad line range: " + start.print + ".." + stop.print) |
|
57 |
||
64647 | 58 |
def print: String = |
59 |
if (start == stop) start.print |
|
60 |
else start.print + ".." + stop.print |
|
64605 | 61 |
} |
62 |
||
63 |
||
64649 | 64 |
/* positions within document node */ |
65 |
||
64651 | 66 |
sealed case class Node_Position(name: String, pos: Position = Position.zero) |
64650 | 67 |
{ |
68 |
def line: Int = pos.line |
|
69 |
def column: Int = pos.column |
|
70 |
} |
|
71 |
||
64651 | 72 |
sealed case class Node_Range(name: String, range: Range = Range.zero) |
64650 | 73 |
{ |
74 |
def start: Position = range.start |
|
75 |
def stop: Position = range.stop |
|
76 |
} |
|
64649 | 77 |
|
78 |
||
64605 | 79 |
/* document with newline as separator (not terminator) */ |
80 |
||
81 |
object Document |
|
82 |
{ |
|
64672 | 83 |
val empty: Document = new Document(Nil) |
64605 | 84 |
|
85 |
def apply(lines: List[Line]): Document = |
|
86 |
if (lines.isEmpty) empty |
|
64672 | 87 |
else new Document(lines) |
64605 | 88 |
|
89 |
def apply(text: String): Document = |
|
64672 | 90 |
if (text == "") empty |
91 |
else if (text.contains('\r')) |
|
92 |
new Document(Library.split_lines(text).map(s => Line(Library.trim_line(s)))) |
|
93 |
else |
|
94 |
new Document(Library.split_lines(text).map(s => Line(s))) |
|
64605 | 95 |
} |
96 |
||
64672 | 97 |
final class Document private(val lines: List[Line]) |
64605 | 98 |
{ |
64672 | 99 |
def make_text: String = lines.mkString("", "\n", "") |
100 |
||
101 |
override def toString: String = make_text |
|
64605 | 102 |
|
103 |
override def equals(that: Any): Boolean = |
|
104 |
that match { |
|
105 |
case other: Document => lines == other.lines |
|
106 |
case _ => false |
|
107 |
} |
|
108 |
override def hashCode(): Int = lines.hashCode |
|
109 |
||
64682 | 110 |
def position(text_offset: Text.Offset, text_length: Text.Length): Position = |
64605 | 111 |
{ |
112 |
@tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position = |
|
113 |
{ |
|
114 |
lines_rest match { |
|
64650 | 115 |
case Nil => require(i == 0); Position(lines_count) |
64605 | 116 |
case line :: ls => |
117 |
val n = line.text.length |
|
64617 | 118 |
if (ls.isEmpty || i <= n) |
64681
642b6105e6f4
clarified signature: explicit Length to avoid implicit mistakes;
wenzelm
parents:
64679
diff
changeset
|
119 |
Position(lines_count).advance(line.text.substring(n - i), text_length) |
64605 | 120 |
else move(i - (n + 1), lines_count + 1, ls) |
121 |
} |
|
122 |
} |
|
64681
642b6105e6f4
clarified signature: explicit Length to avoid implicit mistakes;
wenzelm
parents:
64679
diff
changeset
|
123 |
move(text_offset, 0, lines) |
64605 | 124 |
} |
125 |
||
64682 | 126 |
def range(text_range: Text.Range, text_length: Text.Length): Range = |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64672
diff
changeset
|
127 |
Range( |
64681
642b6105e6f4
clarified signature: explicit Length to avoid implicit mistakes;
wenzelm
parents:
64679
diff
changeset
|
128 |
position(text_range.start, text_length), |
642b6105e6f4
clarified signature: explicit Length to avoid implicit mistakes;
wenzelm
parents:
64679
diff
changeset
|
129 |
position(text_range.stop, text_length)) |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64672
diff
changeset
|
130 |
|
64682 | 131 |
def offset(pos: Position, text_length: Text.Length): Option[Text.Offset] = |
64605 | 132 |
{ |
133 |
val l = pos.line |
|
134 |
val c = pos.column |
|
135 |
if (0 <= l && l < lines.length) { |
|
136 |
val line_offset = |
|
137 |
if (l == 0) 0 |
|
64681
642b6105e6f4
clarified signature: explicit Length to avoid implicit mistakes;
wenzelm
parents:
64679
diff
changeset
|
138 |
else (0 /: lines.iterator.take(l - 1)) { case (n, line) => n + text_length(line.text) + 1 } |
642b6105e6f4
clarified signature: explicit Length to avoid implicit mistakes;
wenzelm
parents:
64679
diff
changeset
|
139 |
text_length.offset(lines(l).text, c).map(line_offset + _) |
64605 | 140 |
} |
141 |
else None |
|
142 |
} |
|
143 |
} |
|
144 |
||
145 |
||
146 |
/* line text */ |
|
147 |
||
148 |
val empty: Line = new Line("") |
|
149 |
def apply(text: String): Line = if (text == "") empty else new Line(text) |
|
150 |
} |
|
151 |
||
152 |
final class Line private(val text: String) |
|
153 |
{ |
|
154 |
require(text.forall(c => c != '\r' && c != '\n')) |
|
155 |
||
64610 | 156 |
lazy val length_codepoints: Int = Codepoint.iterator(text).length |
64605 | 157 |
|
158 |
override def equals(that: Any): Boolean = |
|
159 |
that match { |
|
160 |
case other: Line => text == other.text |
|
161 |
case _ => false |
|
162 |
} |
|
163 |
override def hashCode(): Int = text.hashCode |
|
164 |
override def toString: String = text |
|
165 |
} |