1 /* Title: Tools/VSCode/src/line.scala |
|
2 Author: Makarius |
|
3 |
|
4 Line-oriented text. |
|
5 */ |
|
6 |
|
7 package isabelle.vscode |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import scala.annotation.tailrec |
|
13 |
|
14 |
|
15 object Line |
|
16 { |
|
17 /* position */ |
|
18 |
|
19 object Position |
|
20 { |
|
21 val zero: Position = Position(0, 0) |
|
22 } |
|
23 |
|
24 sealed case class Position(line: Int, column: Int) |
|
25 { |
|
26 def line1: Int = line + 1 |
|
27 def column1: Int = column + 1 |
|
28 def print: String = line1.toString + ":" + column1.toString |
|
29 |
|
30 def compare(that: Position): Int = |
|
31 line compare that.line match { |
|
32 case 0 => column compare that.column |
|
33 case i => i |
|
34 } |
|
35 |
|
36 private def advance[A](iterator: Iterator[A], is_newline: A => Boolean): Position = |
|
37 { |
|
38 var l = line |
|
39 var c = column |
|
40 for (x <- iterator) { |
|
41 if (is_newline(x)) { l += 1; c = 0 } else c += 1 |
|
42 } |
|
43 Position(l, c) |
|
44 } |
|
45 |
|
46 def advance(text: String): Position = |
|
47 if (text.isEmpty) this else advance[Char](text.iterator, _ == '\n') |
|
48 |
|
49 def advance_symbols(text: String): Position = |
|
50 if (text.isEmpty) this else advance[Symbol.Symbol](Symbol.iterator(text), Symbol.is_newline _) |
|
51 |
|
52 def advance_codepoints(text: String): Position = |
|
53 if (text.isEmpty) this else advance[Int](Word.codepoint_iterator(text), _ == 10) |
|
54 } |
|
55 |
|
56 |
|
57 /* range (right-open interval) */ |
|
58 |
|
59 sealed case class Range(start: Position, stop: Position) |
|
60 { |
|
61 if (start.compare(stop) > 0) |
|
62 error("Bad line range: " + start.print + ".." + stop.print) |
|
63 |
|
64 def print: String = start.print + ".." + stop.print |
|
65 } |
|
66 |
|
67 |
|
68 /* document with newline as separator (not terminator) */ |
|
69 |
|
70 object Document |
|
71 { |
|
72 val empty: Document = new Document("", Nil) |
|
73 |
|
74 def apply(lines: List[Line]): Document = |
|
75 if (lines.isEmpty) empty |
|
76 else new Document(lines.mkString("", "\n", ""), lines) |
|
77 |
|
78 def apply(text: String): Document = |
|
79 if (text.contains('\r')) |
|
80 apply(Library.cat_lines(Library.split_lines(text).map(Library.trim_line(_)))) |
|
81 else if (text == "") Document.empty |
|
82 else new Document(text, Library.split_lines(text).map(Line(_))) |
|
83 } |
|
84 |
|
85 final class Document private(val text: String, val lines: List[Line]) |
|
86 { |
|
87 override def toString: String = text |
|
88 |
|
89 override def equals(that: Any): Boolean = |
|
90 that match { |
|
91 case other: Document => lines == other.lines |
|
92 case _ => false |
|
93 } |
|
94 override def hashCode(): Int = lines.hashCode |
|
95 |
|
96 private def position(advance: (Position, String) => Position, offset: Text.Offset): Position = |
|
97 { |
|
98 @tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position = |
|
99 { |
|
100 lines_rest match { |
|
101 case Nil => require(i == 0); Position(lines_count, 0) |
|
102 case line :: ls => |
|
103 val n = line.text.length |
|
104 if (ls.isEmpty || i <= n) advance(Position(lines_count, 0), line.text.substring(n - i)) |
|
105 else move(i - (n + 1), lines_count + 1, ls) |
|
106 } |
|
107 } |
|
108 move(offset, 0, lines) |
|
109 } |
|
110 |
|
111 def position(i: Text.Offset): Position = position(_.advance(_), i) |
|
112 def position_symbols(i: Text.Offset): Position = position(_.advance_symbols(_), i) |
|
113 def position_codepoints(i: Text.Offset): Position = position(_.advance_codepoints(_), i) |
|
114 |
|
115 // FIXME symbols, codepoints |
|
116 def offset(pos: Position): Option[Text.Offset] = |
|
117 { |
|
118 val l = pos.line |
|
119 val c = pos.column |
|
120 if (0 <= l && l < lines.length) { |
|
121 val line_offset = |
|
122 if (l == 0) 0 |
|
123 else (0 /: lines.take(l - 1))({ case (n, line) => n + line.text.length + 1 }) |
|
124 if (c <= lines(l).text.length) Some(line_offset + c) else None |
|
125 } |
|
126 else None |
|
127 } |
|
128 } |
|
129 |
|
130 |
|
131 /* line text */ |
|
132 |
|
133 val empty: Line = new Line("") |
|
134 def apply(text: String): Line = if (text == "") empty else new Line(text) |
|
135 } |
|
136 |
|
137 final class Line private(val text: String) |
|
138 { |
|
139 require(text.forall(c => c != '\r' && c != '\n')) |
|
140 |
|
141 lazy val length_symbols: Int = Symbol.iterator(text).length |
|
142 lazy val length_codepoints: Int = Word.codepoint_iterator(text).length |
|
143 |
|
144 override def equals(that: Any): Boolean = |
|
145 that match { |
|
146 case other: Line => text == other.text |
|
147 case _ => false |
|
148 } |
|
149 override def hashCode(): Int = text.hashCode |
|
150 override def toString: String = text |
|
151 } |
|