author | wenzelm |
Mon, 01 Mar 2021 22:22:12 +0100 | |
changeset 73340 | 0ffcad1f6130 |
parent 66114 | c137a9f038a6 |
child 75393 | 87ebf5a50283 |
permissions | -rw-r--r-- |
38425 | 1 |
/* Title: Pure/PIDE/text.scala |
34276 | 2 |
Author: Fabian Immler, TU Munich |
3 |
Author: Makarius |
|
4 |
||
38425 | 5 |
Basic operations on plain text. |
34276 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
44379 | 11 |
import scala.collection.mutable |
12 |
import scala.util.Sorting |
|
13 |
||
14 |
||
38425 | 15 |
object Text |
34276 | 16 |
{ |
38477 | 17 |
/* offset */ |
38426 | 18 |
|
19 |
type Offset = Int |
|
20 |
||
38477 | 21 |
|
38565
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38564
diff
changeset
|
22 |
/* range -- with total quasi-ordering */ |
38477 | 23 |
|
38568 | 24 |
object Range |
25 |
{ |
|
26 |
def apply(start: Offset): Range = Range(start, start) |
|
44379 | 27 |
|
64678 | 28 |
val full: Range = apply(0, Integer.MAX_VALUE / 2) |
56172 | 29 |
val offside: Range = apply(-1) |
30 |
||
65154 | 31 |
object Ordering extends scala.math.Ordering[Range] |
44379 | 32 |
{ |
65154 | 33 |
def compare(r1: Range, r2: Range): Int = r1 compare r2 |
44379 | 34 |
} |
38568 | 35 |
} |
36 |
||
60215 | 37 |
sealed case class Range(start: Offset, stop: Offset) |
38427 | 38 |
{ |
38565
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38564
diff
changeset
|
39 |
// denotation: {start} Un {i. start < i & i < stop} |
43425 | 40 |
if (start > stop) |
64546
134ae7da2ccf
clarified output: avoid confusion with line:column notation;
wenzelm
parents:
64370
diff
changeset
|
41 |
error("Bad range: [" + start.toString + ".." + stop.toString + "]") |
38477 | 42 |
|
64546
134ae7da2ccf
clarified output: avoid confusion with line:column notation;
wenzelm
parents:
64370
diff
changeset
|
43 |
override def toString: String = "[" + start.toString + ".." + stop.toString + "]" |
38563 | 44 |
|
65155
25bccf5bf33e
clarified native Text.Offset versus Text.Length index Int;
wenzelm
parents:
65154
diff
changeset
|
45 |
def length: Offset = stop - start |
47542
26d0a76fef0a
more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);
wenzelm
parents:
46712
diff
changeset
|
46 |
|
38427 | 47 |
def map(f: Offset => Offset): Range = Range(f(start), f(stop)) |
56308 | 48 |
def +(i: Offset): Range = if (i == 0) this else map(_ + i) |
49 |
def -(i: Offset): Range = if (i == 0) this else map(_ - i) |
|
38662 | 50 |
|
38725 | 51 |
def is_singularity: Boolean = start == stop |
56590
d01d183e84ea
clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
wenzelm
parents:
56473
diff
changeset
|
52 |
def inflate_singularity: Range = if (is_singularity) Range(start, start + 1) else this |
38662 | 53 |
|
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
57912
diff
changeset
|
54 |
def touches(i: Offset): Boolean = start <= i && i <= stop |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
57912
diff
changeset
|
55 |
|
38565
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38564
diff
changeset
|
56 |
def contains(i: Offset): Boolean = start == i || start < i && i < stop |
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38564
diff
changeset
|
57 |
def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop |
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38564
diff
changeset
|
58 |
def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start) |
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38564
diff
changeset
|
59 |
def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start |
38485 | 60 |
|
45240
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
61 |
def apart(that: Range): Boolean = |
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
62 |
(this.start max that.start) > (this.stop min that.stop) |
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
63 |
|
38564 | 64 |
def restrict(that: Range): Range = |
38485 | 65 |
Range(this.start max that.start, this.stop min that.stop) |
43428
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
66 |
|
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
67 |
def try_restrict(that: Range): Option[Range] = |
45240
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
68 |
if (this apart that) None |
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
69 |
else Some(restrict(that)) |
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
70 |
|
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
71 |
def try_join(that: Range): Option[Range] = |
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
72 |
if (this apart that) None |
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
73 |
else Some(Range(this.start min that.start, this.stop max that.stop)) |
65522 | 74 |
|
75 |
def substring(text: String): String = text.substring(start, stop) |
|
66114 | 76 |
|
77 |
def try_substring(text: String): Option[String] = |
|
78 |
try { Some(substring(text)) } |
|
79 |
catch { case _: IndexOutOfBoundsException => None } |
|
38427 | 80 |
} |
38426 | 81 |
|
82 |
||
44379 | 83 |
/* perspective */ |
84 |
||
44473 | 85 |
object Perspective |
44379 | 86 |
{ |
44474 | 87 |
val empty: Perspective = Perspective(Nil) |
44379 | 88 |
|
64678 | 89 |
def full: Perspective = Perspective(List(Range.full)) |
46576
ae9286f64574
approximate Perspective.full within the bounds of the JVM;
wenzelm
parents:
46207
diff
changeset
|
90 |
|
65371 | 91 |
def apply(ranges: List[Range]): Perspective = |
44379 | 92 |
{ |
65154 | 93 |
val result = new mutable.ListBuffer[Range] |
94 |
var last: Option[Range] = None |
|
73340 | 95 |
def ship(next: Option[Range]): Unit = { result ++= last; last = next } |
45240
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
96 |
|
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
97 |
for (range <- ranges.sortBy(_.start)) |
44473 | 98 |
{ |
99 |
last match { |
|
45240
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
100 |
case None => ship(Some(range)) |
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
101 |
case Some(last_range) => |
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
102 |
last_range.try_join(range) match { |
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
103 |
case None => ship(Some(range)) |
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
104 |
case joined => last = joined |
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
105 |
} |
44473 | 106 |
} |
44379 | 107 |
} |
45240
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
108 |
ship(None) |
44473 | 109 |
new Perspective(result.toList) |
44379 | 110 |
} |
44473 | 111 |
} |
112 |
||
46712 | 113 |
final class Perspective private( |
114 |
val ranges: List[Range]) // visible text partitioning in canonical order |
|
44473 | 115 |
{ |
116 |
def is_empty: Boolean = ranges.isEmpty |
|
117 |
def range: Range = |
|
118 |
if (is_empty) Range(0) |
|
119 |
else Range(ranges.head.start, ranges.last.stop) |
|
45631
6bdf8b926f50
recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;
wenzelm
parents:
45470
diff
changeset
|
120 |
|
6bdf8b926f50
recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;
wenzelm
parents:
45470
diff
changeset
|
121 |
override def hashCode: Int = ranges.hashCode |
6bdf8b926f50
recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;
wenzelm
parents:
45470
diff
changeset
|
122 |
override def equals(that: Any): Boolean = |
6bdf8b926f50
recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;
wenzelm
parents:
45470
diff
changeset
|
123 |
that match { |
6bdf8b926f50
recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;
wenzelm
parents:
45470
diff
changeset
|
124 |
case other: Perspective => ranges == other.ranges |
6bdf8b926f50
recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;
wenzelm
parents:
45470
diff
changeset
|
125 |
case _ => false |
6bdf8b926f50
recovered structural equality from 9d97bd3c086a, otherwise update_perspective might be issued over and over again, canceling a pending/slow execution;
wenzelm
parents:
45470
diff
changeset
|
126 |
} |
57912 | 127 |
override def toString: String = ranges.toString |
44379 | 128 |
} |
129 |
||
130 |
||
38577 | 131 |
/* information associated with text range */ |
132 |
||
65154 | 133 |
sealed case class Info[A](range: Range, info: A) |
38577 | 134 |
{ |
65154 | 135 |
def restrict(r: Range): Info[A] = Info(range.restrict(r), info) |
136 |
def try_restrict(r: Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info)) |
|
65132 | 137 |
|
138 |
def map[B](f: A => B): Info[B] = Info(range, f(info)) |
|
38577 | 139 |
} |
140 |
||
45470 | 141 |
type Markup = Info[XML.Elem] |
45455 | 142 |
|
38577 | 143 |
|
38426 | 144 |
/* editing */ |
34286 | 145 |
|
38425 | 146 |
object Edit |
147 |
{ |
|
38426 | 148 |
def insert(start: Offset, text: String): Edit = new Edit(true, start, text) |
149 |
def remove(start: Offset, text: String): Edit = new Edit(false, start, text) |
|
65156 | 150 |
def inserts(start: Offset, text: String): List[Edit] = |
151 |
if (text == "") Nil else List(insert(start, text)) |
|
152 |
def removes(start: Offset, text: String): List[Edit] = |
|
153 |
if (text == "") Nil else List(remove(start, text)) |
|
64816 | 154 |
def replace(start: Offset, old_text: String, new_text: String): List[Edit] = |
155 |
if (old_text == new_text) Nil |
|
65156 | 156 |
else removes(start, old_text) ::: inserts(start, new_text) |
38425 | 157 |
} |
34286 | 158 |
|
46712 | 159 |
final class Edit private(val is_insert: Boolean, val start: Offset, val text: String) |
38425 | 160 |
{ |
57912 | 161 |
override def toString: String = |
38425 | 162 |
(if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" |
34286 | 163 |
|
164 |
||
38425 | 165 |
/* transform offsets */ |
34286 | 166 |
|
38426 | 167 |
private def transform(do_insert: Boolean, i: Offset): Offset = |
168 |
if (i < start) i |
|
43425 | 169 |
else if (do_insert) i + text.length |
38426 | 170 |
else (i - text.length) max start |
34286 | 171 |
|
43425 | 172 |
def convert(i: Offset): Offset = transform(is_insert, i) |
173 |
def revert(i: Offset): Offset = transform(!is_insert, i) |
|
38425 | 174 |
|
34286 | 175 |
|
38425 | 176 |
/* edit strings */ |
177 |
||
38426 | 178 |
private def insert(i: Offset, string: String): String = |
179 |
string.substring(0, i) + text + string.substring(i) |
|
34276 | 180 |
|
65155
25bccf5bf33e
clarified native Text.Offset versus Text.Length index Int;
wenzelm
parents:
65154
diff
changeset
|
181 |
private def remove(i: Offset, count: Offset, string: String): String = |
38426 | 182 |
string.substring(0, i) + string.substring(i + count) |
38425 | 183 |
|
65155
25bccf5bf33e
clarified native Text.Offset versus Text.Length index Int;
wenzelm
parents:
65154
diff
changeset
|
184 |
def can_edit(string: String, shift: Offset): Boolean = |
38425 | 185 |
shift <= start && start < shift + string.length |
186 |
||
65155
25bccf5bf33e
clarified native Text.Offset versus Text.Length index Int;
wenzelm
parents:
65154
diff
changeset
|
187 |
def edit(string: String, shift: Offset): (Option[Edit], String) = |
38425 | 188 |
if (!can_edit(string, shift)) (Some(this), string) |
189 |
else if (is_insert) (None, insert(start - shift, string)) |
|
190 |
else { |
|
38426 | 191 |
val i = start - shift |
192 |
val count = text.length min (string.length - i) |
|
38425 | 193 |
val rest = |
194 |
if (count == text.length) None |
|
195 |
else Some(Edit.remove(start, text.substring(count))) |
|
38426 | 196 |
(rest, remove(i, count, string)) |
38425 | 197 |
} |
198 |
} |
|
34276 | 199 |
} |