author | wenzelm |
Mon, 22 Aug 2011 21:42:02 +0200 | |
changeset 44384 | 8f6054a63f96 |
parent 44379 | 1079ab6b342b |
child 44473 | 4f264fdf8d0e |
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.math.Ordering |
|
13 |
import scala.util.Sorting |
|
14 |
||
15 |
||
38425 | 16 |
object Text |
34276 | 17 |
{ |
38477 | 18 |
/* offset */ |
38426 | 19 |
|
20 |
type Offset = Int |
|
21 |
||
38477 | 22 |
|
38565
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38564
diff
changeset
|
23 |
/* range -- with total quasi-ordering */ |
38477 | 24 |
|
38568 | 25 |
object Range |
26 |
{ |
|
27 |
def apply(start: Offset): Range = Range(start, start) |
|
44379 | 28 |
|
29 |
object Ordering extends scala.math.Ordering[Text.Range] |
|
30 |
{ |
|
31 |
def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2 |
|
32 |
} |
|
38568 | 33 |
} |
34 |
||
38426 | 35 |
sealed case class Range(val start: Offset, val stop: Offset) |
38427 | 36 |
{ |
38565
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38564
diff
changeset
|
37 |
// denotation: {start} Un {i. start < i & i < stop} |
43425 | 38 |
if (start > stop) |
39 |
error("Bad range: [" + start.toString + ":" + stop.toString + "]") |
|
38477 | 40 |
|
38563 | 41 |
override def toString = "[" + start.toString + ":" + stop.toString + "]" |
42 |
||
38427 | 43 |
def map(f: Offset => Offset): Range = Range(f(start), f(stop)) |
44 |
def +(i: Offset): Range = map(_ + i) |
|
38570 | 45 |
def -(i: Offset): Range = map(_ - i) |
38662 | 46 |
|
38725 | 47 |
def is_singularity: Boolean = start == stop |
38662 | 48 |
|
38565
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38564
diff
changeset
|
49 |
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
|
50 |
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
|
51 |
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
|
52 |
def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start |
38485 | 53 |
|
38564 | 54 |
def restrict(that: Range): Range = |
38485 | 55 |
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
|
56 |
|
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
57 |
def try_restrict(that: Range): Option[Range] = |
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
58 |
try { Some (restrict(that)) } |
43650 | 59 |
catch { case ERROR(_) => None } |
38427 | 60 |
} |
38426 | 61 |
|
62 |
||
44379 | 63 |
/* perspective */ |
64 |
||
44384 | 65 |
type Perspective = List[Range] // visible text partitioning in canonical order |
44379 | 66 |
|
67 |
def perspective(ranges: Seq[Range]): Perspective = |
|
68 |
{ |
|
69 |
val sorted_ranges = ranges.toArray |
|
70 |
Sorting.quickSort(sorted_ranges)(Range.Ordering) |
|
71 |
||
72 |
val result = new mutable.ListBuffer[Text.Range] |
|
73 |
var last: Option[Text.Range] = None |
|
74 |
for (range <- sorted_ranges) |
|
75 |
{ |
|
76 |
last match { |
|
77 |
case Some(last_range) |
|
78 |
if ((last_range overlaps range) || last_range.stop == range.start) => |
|
79 |
last = Some(Text.Range(last_range.start, range.stop)) |
|
80 |
case _ => |
|
81 |
result ++= last |
|
82 |
last = Some(range) |
|
83 |
} |
|
84 |
} |
|
85 |
result ++= last |
|
86 |
result.toList |
|
87 |
} |
|
88 |
||
89 |
||
38577 | 90 |
/* information associated with text range */ |
91 |
||
43714 | 92 |
sealed case class Info[A](val range: Text.Range, val info: A) |
38577 | 93 |
{ |
94 |
def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info) |
|
43428
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
95 |
def try_restrict(r: Text.Range): Option[Info[A]] = |
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
96 |
try { Some(Info(range.restrict(r), info)) } |
43650 | 97 |
catch { case ERROR(_) => None } |
38577 | 98 |
} |
99 |
||
100 |
||
38426 | 101 |
/* editing */ |
34286 | 102 |
|
38425 | 103 |
object Edit |
104 |
{ |
|
38426 | 105 |
def insert(start: Offset, text: String): Edit = new Edit(true, start, text) |
106 |
def remove(start: Offset, text: String): Edit = new Edit(false, start, text) |
|
38425 | 107 |
} |
34286 | 108 |
|
38426 | 109 |
class Edit(val is_insert: Boolean, val start: Offset, val text: String) |
38425 | 110 |
{ |
111 |
override def toString = |
|
112 |
(if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" |
|
34286 | 113 |
|
114 |
||
38425 | 115 |
/* transform offsets */ |
34286 | 116 |
|
38426 | 117 |
private def transform(do_insert: Boolean, i: Offset): Offset = |
118 |
if (i < start) i |
|
43425 | 119 |
else if (do_insert) i + text.length |
38426 | 120 |
else (i - text.length) max start |
34286 | 121 |
|
43425 | 122 |
def convert(i: Offset): Offset = transform(is_insert, i) |
123 |
def revert(i: Offset): Offset = transform(!is_insert, i) |
|
124 |
def convert(range: Range): Range = range.map(convert) |
|
125 |
def revert(range: Range): Range = range.map(revert) |
|
38425 | 126 |
|
34286 | 127 |
|
38425 | 128 |
/* edit strings */ |
129 |
||
38426 | 130 |
private def insert(i: Offset, string: String): String = |
131 |
string.substring(0, i) + text + string.substring(i) |
|
34276 | 132 |
|
38426 | 133 |
private def remove(i: Offset, count: Int, string: String): String = |
134 |
string.substring(0, i) + string.substring(i + count) |
|
38425 | 135 |
|
136 |
def can_edit(string: String, shift: Int): Boolean = |
|
137 |
shift <= start && start < shift + string.length |
|
138 |
||
139 |
def edit(string: String, shift: Int): (Option[Edit], String) = |
|
140 |
if (!can_edit(string, shift)) (Some(this), string) |
|
141 |
else if (is_insert) (None, insert(start - shift, string)) |
|
142 |
else { |
|
38426 | 143 |
val i = start - shift |
144 |
val count = text.length min (string.length - i) |
|
38425 | 145 |
val rest = |
146 |
if (count == text.length) None |
|
147 |
else Some(Edit.remove(start, text.substring(count))) |
|
38426 | 148 |
(rest, remove(i, count, string)) |
38425 | 149 |
} |
150 |
} |
|
34276 | 151 |
} |