author | wenzelm |
Sat, 18 Jun 2011 00:05:29 +0200 | |
changeset 43428 | b41dea5772c6 |
parent 43425 | 0a5612040a8b |
child 43650 | f00da558b78e |
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 |
||
38425 | 11 |
object Text |
34276 | 12 |
{ |
38477 | 13 |
/* offset */ |
38426 | 14 |
|
15 |
type Offset = Int |
|
16 |
||
38477 | 17 |
|
38565
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38564
diff
changeset
|
18 |
/* range -- with total quasi-ordering */ |
38477 | 19 |
|
38568 | 20 |
object Range |
21 |
{ |
|
22 |
def apply(start: Offset): Range = Range(start, start) |
|
23 |
} |
|
24 |
||
38426 | 25 |
sealed case class Range(val start: Offset, val stop: Offset) |
38427 | 26 |
{ |
38565
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38564
diff
changeset
|
27 |
// denotation: {start} Un {i. start < i & i < stop} |
43425 | 28 |
if (start > stop) |
29 |
error("Bad range: [" + start.toString + ":" + stop.toString + "]") |
|
38477 | 30 |
|
38563 | 31 |
override def toString = "[" + start.toString + ":" + stop.toString + "]" |
32 |
||
38427 | 33 |
def map(f: Offset => Offset): Range = Range(f(start), f(stop)) |
34 |
def +(i: Offset): Range = map(_ + i) |
|
38570 | 35 |
def -(i: Offset): Range = map(_ - i) |
38662 | 36 |
|
38725 | 37 |
def is_singularity: Boolean = start == stop |
38662 | 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 |
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
|
40 |
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
|
41 |
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
|
42 |
def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start |
38485 | 43 |
|
38564 | 44 |
def restrict(that: Range): Range = |
38485 | 45 |
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
|
46 |
|
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
47 |
def try_restrict(that: Range): Option[Range] = |
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
48 |
try { Some (restrict(that)) } |
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
49 |
catch { case _: RuntimeException => None } |
38427 | 50 |
} |
38426 | 51 |
|
52 |
||
38577 | 53 |
/* information associated with text range */ |
54 |
||
55 |
case class Info[A](val range: Text.Range, val info: A) |
|
56 |
{ |
|
57 |
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
|
58 |
def try_restrict(r: Text.Range): Option[Info[A]] = |
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
59 |
try { Some(Info(range.restrict(r), info)) } |
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
60 |
catch { case _: RuntimeException => None } |
38577 | 61 |
} |
62 |
||
63 |
||
38426 | 64 |
/* editing */ |
34286 | 65 |
|
38425 | 66 |
object Edit |
67 |
{ |
|
38426 | 68 |
def insert(start: Offset, text: String): Edit = new Edit(true, start, text) |
69 |
def remove(start: Offset, text: String): Edit = new Edit(false, start, text) |
|
38425 | 70 |
} |
34286 | 71 |
|
38426 | 72 |
class Edit(val is_insert: Boolean, val start: Offset, val text: String) |
38425 | 73 |
{ |
74 |
override def toString = |
|
75 |
(if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" |
|
34286 | 76 |
|
77 |
||
38425 | 78 |
/* transform offsets */ |
34286 | 79 |
|
38426 | 80 |
private def transform(do_insert: Boolean, i: Offset): Offset = |
81 |
if (i < start) i |
|
43425 | 82 |
else if (do_insert) i + text.length |
38426 | 83 |
else (i - text.length) max start |
34286 | 84 |
|
43425 | 85 |
def convert(i: Offset): Offset = transform(is_insert, i) |
86 |
def revert(i: Offset): Offset = transform(!is_insert, i) |
|
87 |
def convert(range: Range): Range = range.map(convert) |
|
88 |
def revert(range: Range): Range = range.map(revert) |
|
38425 | 89 |
|
34286 | 90 |
|
38425 | 91 |
/* edit strings */ |
92 |
||
38426 | 93 |
private def insert(i: Offset, string: String): String = |
94 |
string.substring(0, i) + text + string.substring(i) |
|
34276 | 95 |
|
38426 | 96 |
private def remove(i: Offset, count: Int, string: String): String = |
97 |
string.substring(0, i) + string.substring(i + count) |
|
38425 | 98 |
|
99 |
def can_edit(string: String, shift: Int): Boolean = |
|
100 |
shift <= start && start < shift + string.length |
|
101 |
||
102 |
def edit(string: String, shift: Int): (Option[Edit], String) = |
|
103 |
if (!can_edit(string, shift)) (Some(this), string) |
|
104 |
else if (is_insert) (None, insert(start - shift, string)) |
|
105 |
else { |
|
38426 | 106 |
val i = start - shift |
107 |
val count = text.length min (string.length - i) |
|
38425 | 108 |
val rest = |
109 |
if (count == text.length) None |
|
110 |
else Some(Edit.remove(start, text.substring(count))) |
|
38426 | 111 |
(rest, remove(i, count, string)) |
38425 | 112 |
} |
113 |
} |
|
34276 | 114 |
} |