author | wenzelm |
Sat, 07 Jan 2017 17:30:06 +0100 | |
changeset 64821 | 37bf7acf6a4b |
parent 64820 | 00488a8c042f |
child 64822 | c8bac4b0ef07 |
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 |
{ |
|
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 |
||
64682 | 43 |
def advance(text: String, text_length: Text.Length): Position = |
64617 | 44 |
if (text.isEmpty) this |
45 |
else { |
|
64806 | 46 |
val lines = logical_lines(text) |
64619 | 47 |
val l = line + lines.length - 1 |
64681
642b6105e6f4
clarified signature: explicit Length to avoid implicit mistakes;
wenzelm
parents:
64679
diff
changeset
|
48 |
val c = (if (l == line) column else 0) + text_length(Library.trim_line(lines.last)) |
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 |
{ |
|
64683
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64682
diff
changeset
|
92 |
def apply(text: String, text_length: Text.Length): Document = |
64820
00488a8c042f
Line.Document consists of independently allocated strings;
wenzelm
parents:
64806
diff
changeset
|
93 |
Document(logical_lines(text).map(s => Line(Library.trim_substring(s))), text_length) |
64605 | 94 |
} |
95 |
||
64683
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64682
diff
changeset
|
96 |
sealed case class Document(lines: List[Line], text_length: Text.Length) |
64605 | 97 |
{ |
64821 | 98 |
lazy val text: String = lines.mkString("", "\n", "") |
99 |
lazy val bytes: Bytes = Bytes(text) |
|
100 |
lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) |
|
64672 | 101 |
|
64821 | 102 |
lazy val length: Int = |
103 |
if (lines.isEmpty) 0 |
|
104 |
else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1 |
|
105 |
||
106 |
def text_range: Text.Range = Text.Range(0, length) |
|
107 |
||
108 |
override def toString: String = text |
|
64605 | 109 |
|
110 |
override def equals(that: Any): Boolean = |
|
111 |
that match { |
|
112 |
case other: Document => lines == other.lines |
|
113 |
case _ => false |
|
114 |
} |
|
115 |
override def hashCode(): Int = lines.hashCode |
|
116 |
||
64683
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64682
diff
changeset
|
117 |
def position(text_offset: Text.Offset): Position = |
64605 | 118 |
{ |
119 |
@tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position = |
|
120 |
{ |
|
121 |
lines_rest match { |
|
64650 | 122 |
case Nil => require(i == 0); Position(lines_count) |
64605 | 123 |
case line :: ls => |
124 |
val n = line.text.length |
|
64617 | 125 |
if (ls.isEmpty || i <= n) |
64681
642b6105e6f4
clarified signature: explicit Length to avoid implicit mistakes;
wenzelm
parents:
64679
diff
changeset
|
126 |
Position(lines_count).advance(line.text.substring(n - i), text_length) |
64605 | 127 |
else move(i - (n + 1), lines_count + 1, ls) |
128 |
} |
|
129 |
} |
|
64681
642b6105e6f4
clarified signature: explicit Length to avoid implicit mistakes;
wenzelm
parents:
64679
diff
changeset
|
130 |
move(text_offset, 0, lines) |
64605 | 131 |
} |
132 |
||
64683
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64682
diff
changeset
|
133 |
def range(text_range: Text.Range): Range = |
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64682
diff
changeset
|
134 |
Range(position(text_range.start), position(text_range.stop)) |
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64672
diff
changeset
|
135 |
|
64683
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64682
diff
changeset
|
136 |
def offset(pos: Position): Option[Text.Offset] = |
64605 | 137 |
{ |
138 |
val l = pos.line |
|
139 |
val c = pos.column |
|
140 |
if (0 <= l && l < lines.length) { |
|
141 |
val line_offset = |
|
64763 | 142 |
(0 /: lines.iterator.take(l)) { case (n, line) => n + text_length(line.text) + 1 } |
64681
642b6105e6f4
clarified signature: explicit Length to avoid implicit mistakes;
wenzelm
parents:
64679
diff
changeset
|
143 |
text_length.offset(lines(l).text, c).map(line_offset + _) |
64605 | 144 |
} |
145 |
else None |
|
146 |
} |
|
147 |
} |
|
148 |
||
149 |
||
150 |
/* line text */ |
|
151 |
||
152 |
val empty: Line = new Line("") |
|
153 |
def apply(text: String): Line = if (text == "") empty else new Line(text) |
|
154 |
} |
|
155 |
||
156 |
final class Line private(val text: String) |
|
157 |
{ |
|
158 |
require(text.forall(c => c != '\r' && c != '\n')) |
|
159 |
||
160 |
override def equals(that: Any): Boolean = |
|
161 |
that match { |
|
162 |
case other: Line => text == other.text |
|
163 |
case _ => false |
|
164 |
} |
|
165 |
override def hashCode(): Int = text.hashCode |
|
166 |
override def toString: String = text |
|
167 |
} |