author | wenzelm |
Fri, 21 Oct 2011 22:44:55 +0200 | |
changeset 45240 | 9d97bd3c086a |
parent 44474 | 681447a9ffe5 |
child 45250 | feef63bcd787 |
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 |
|
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
|
54 |
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
|
55 |
(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
|
56 |
|
38564 | 57 |
def restrict(that: Range): Range = |
38485 | 58 |
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
|
59 |
|
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
60 |
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
|
61 |
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
|
62 |
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
|
63 |
|
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
64 |
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
|
65 |
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
|
66 |
else Some(Range(this.start min that.start, this.stop max that.stop)) |
38427 | 67 |
} |
38426 | 68 |
|
69 |
||
44379 | 70 |
/* perspective */ |
71 |
||
44473 | 72 |
object Perspective |
44379 | 73 |
{ |
44474 | 74 |
val empty: Perspective = Perspective(Nil) |
44379 | 75 |
|
44473 | 76 |
def apply(ranges: Seq[Range]): Perspective = |
44379 | 77 |
{ |
44473 | 78 |
val result = new mutable.ListBuffer[Text.Range] |
79 |
var last: Option[Text.Range] = None |
|
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
|
80 |
def ship(next: Option[Range]) { result ++= last; last = next } |
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
81 |
|
9d97bd3c086a
proper normal form for Perspective.ranges (overlapping ranges could be joined in wrong order, crashing multiple editor views);
wenzelm
parents:
44474
diff
changeset
|
82 |
for (range <- ranges.sortBy(_.start)) |
44473 | 83 |
{ |
84 |
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
|
85 |
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
|
86 |
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
|
87 |
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
|
88 |
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
|
89 |
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
|
90 |
} |
44473 | 91 |
} |
44379 | 92 |
} |
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
|
93 |
ship(None) |
44473 | 94 |
new Perspective(result.toList) |
44379 | 95 |
} |
44473 | 96 |
} |
97 |
||
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
|
98 |
class Perspective private(val ranges: List[Range]) // visible text partitioning in canonical order |
44473 | 99 |
{ |
100 |
def is_empty: Boolean = ranges.isEmpty |
|
101 |
def range: Range = |
|
102 |
if (is_empty) Range(0) |
|
103 |
else Range(ranges.head.start, ranges.last.stop) |
|
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
|
104 |
override def toString = ranges.toString |
44379 | 105 |
} |
106 |
||
107 |
||
38577 | 108 |
/* information associated with text range */ |
109 |
||
43714 | 110 |
sealed case class Info[A](val range: Text.Range, val info: A) |
38577 | 111 |
{ |
112 |
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
|
113 |
def try_restrict(r: Text.Range): Option[Info[A]] = |
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
114 |
try { Some(Info(range.restrict(r), info)) } |
43650 | 115 |
catch { case ERROR(_) => None } |
38577 | 116 |
} |
117 |
||
118 |
||
38426 | 119 |
/* editing */ |
34286 | 120 |
|
38425 | 121 |
object Edit |
122 |
{ |
|
38426 | 123 |
def insert(start: Offset, text: String): Edit = new Edit(true, start, text) |
124 |
def remove(start: Offset, text: String): Edit = new Edit(false, start, text) |
|
38425 | 125 |
} |
34286 | 126 |
|
38426 | 127 |
class Edit(val is_insert: Boolean, val start: Offset, val text: String) |
38425 | 128 |
{ |
129 |
override def toString = |
|
130 |
(if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" |
|
34286 | 131 |
|
132 |
||
38425 | 133 |
/* transform offsets */ |
34286 | 134 |
|
38426 | 135 |
private def transform(do_insert: Boolean, i: Offset): Offset = |
136 |
if (i < start) i |
|
43425 | 137 |
else if (do_insert) i + text.length |
38426 | 138 |
else (i - text.length) max start |
34286 | 139 |
|
43425 | 140 |
def convert(i: Offset): Offset = transform(is_insert, i) |
141 |
def revert(i: Offset): Offset = transform(!is_insert, i) |
|
142 |
def convert(range: Range): Range = range.map(convert) |
|
143 |
def revert(range: Range): Range = range.map(revert) |
|
38425 | 144 |
|
34286 | 145 |
|
38425 | 146 |
/* edit strings */ |
147 |
||
38426 | 148 |
private def insert(i: Offset, string: String): String = |
149 |
string.substring(0, i) + text + string.substring(i) |
|
34276 | 150 |
|
38426 | 151 |
private def remove(i: Offset, count: Int, string: String): String = |
152 |
string.substring(0, i) + string.substring(i + count) |
|
38425 | 153 |
|
154 |
def can_edit(string: String, shift: Int): Boolean = |
|
155 |
shift <= start && start < shift + string.length |
|
156 |
||
157 |
def edit(string: String, shift: Int): (Option[Edit], String) = |
|
158 |
if (!can_edit(string, shift)) (Some(this), string) |
|
159 |
else if (is_insert) (None, insert(start - shift, string)) |
|
160 |
else { |
|
38426 | 161 |
val i = start - shift |
162 |
val count = text.length min (string.length - i) |
|
38425 | 163 |
val rest = |
164 |
if (count == text.length) None |
|
165 |
else Some(Edit.remove(start, text.substring(count))) |
|
38426 | 166 |
(rest, remove(i, count, string)) |
38425 | 167 |
} |
168 |
} |
|
34276 | 169 |
} |