author | wenzelm |
Sat, 15 Dec 2012 18:30:09 +0100 | |
changeset 50552 | 2b7fd8c9c4ac |
parent 48677 | bd4d132e32cf |
child 56172 | 31289387fdf8 |
permissions | -rw-r--r-- |
38425 | 1 |
/* Title: Pure/PIDE/text.scala |
45673
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents:
45667
diff
changeset
|
2 |
Module: PIDE |
34276 | 3 |
Author: Fabian Immler, TU Munich |
4 |
Author: Makarius |
|
5 |
||
38425 | 6 |
Basic operations on plain text. |
34276 | 7 |
*/ |
8 |
||
9 |
package isabelle |
|
10 |
||
11 |
||
44379 | 12 |
import scala.collection.mutable |
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 |
||
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
|
43 |
def length: Int = stop - start |
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
|
44 |
|
38427 | 45 |
def map(f: Offset => Offset): Range = Range(f(start), f(stop)) |
46 |
def +(i: Offset): Range = map(_ + i) |
|
38570 | 47 |
def -(i: Offset): Range = map(_ - i) |
38662 | 48 |
|
38725 | 49 |
def is_singularity: Boolean = start == stop |
38662 | 50 |
|
38565
32b924a832c4
further clarification/unification of Position.Range and Text.Range concerning singularities: start offset is always included;
wenzelm
parents:
38564
diff
changeset
|
51 |
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
|
52 |
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
|
53 |
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
|
54 |
def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start |
38485 | 55 |
|
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
|
56 |
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
|
57 |
(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
|
58 |
|
38564 | 59 |
def restrict(that: Range): Range = |
38485 | 60 |
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
|
61 |
|
b41dea5772c6
more robust treatment of partial range restriction;
wenzelm
parents:
43425
diff
changeset
|
62 |
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
|
63 |
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
|
64 |
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
|
65 |
|
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 |
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
|
67 |
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
|
68 |
else Some(Range(this.start min that.start, this.stop max that.stop)) |
38427 | 69 |
} |
38426 | 70 |
|
71 |
||
44379 | 72 |
/* perspective */ |
73 |
||
44473 | 74 |
object Perspective |
44379 | 75 |
{ |
44474 | 76 |
val empty: Perspective = Perspective(Nil) |
44379 | 77 |
|
46576
ae9286f64574
approximate Perspective.full within the bounds of the JVM;
wenzelm
parents:
46207
diff
changeset
|
78 |
def full: Perspective = Perspective(List(Range(0, Integer.MAX_VALUE / 2))) |
ae9286f64574
approximate Perspective.full within the bounds of the JVM;
wenzelm
parents:
46207
diff
changeset
|
79 |
|
44473 | 80 |
def apply(ranges: Seq[Range]): Perspective = |
44379 | 81 |
{ |
44473 | 82 |
val result = new mutable.ListBuffer[Text.Range] |
83 |
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
|
84 |
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
|
85 |
|
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 |
for (range <- ranges.sortBy(_.start)) |
44473 | 87 |
{ |
88 |
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
|
89 |
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
|
90 |
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
|
91 |
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
|
92 |
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
|
93 |
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
|
94 |
} |
44473 | 95 |
} |
44379 | 96 |
} |
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
|
97 |
ship(None) |
44473 | 98 |
new Perspective(result.toList) |
44379 | 99 |
} |
44473 | 100 |
} |
101 |
||
46712 | 102 |
final class Perspective private( |
103 |
val ranges: List[Range]) // visible text partitioning in canonical order |
|
44473 | 104 |
{ |
105 |
def is_empty: Boolean = ranges.isEmpty |
|
106 |
def range: Range = |
|
107 |
if (is_empty) Range(0) |
|
108 |
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
|
109 |
|
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
|
110 |
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
|
111 |
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
|
112 |
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
|
113 |
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
|
114 |
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
|
115 |
} |
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
|
116 |
override def toString = ranges.toString |
44379 | 117 |
} |
118 |
||
119 |
||
38577 | 120 |
/* information associated with text range */ |
121 |
||
43714 | 122 |
sealed case class Info[A](val range: Text.Range, val info: A) |
38577 | 123 |
{ |
124 |
def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info) |
|
46207 | 125 |
def try_restrict(r: Text.Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info)) |
38577 | 126 |
} |
127 |
||
45470 | 128 |
type Markup = Info[XML.Elem] |
45455 | 129 |
|
38577 | 130 |
|
38426 | 131 |
/* editing */ |
34286 | 132 |
|
38425 | 133 |
object Edit |
134 |
{ |
|
38426 | 135 |
def insert(start: Offset, text: String): Edit = new Edit(true, start, text) |
136 |
def remove(start: Offset, text: String): Edit = new Edit(false, start, text) |
|
38425 | 137 |
} |
34286 | 138 |
|
46712 | 139 |
final class Edit private(val is_insert: Boolean, val start: Offset, val text: String) |
38425 | 140 |
{ |
141 |
override def toString = |
|
142 |
(if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" |
|
34286 | 143 |
|
144 |
||
38425 | 145 |
/* transform offsets */ |
34286 | 146 |
|
38426 | 147 |
private def transform(do_insert: Boolean, i: Offset): Offset = |
148 |
if (i < start) i |
|
43425 | 149 |
else if (do_insert) i + text.length |
38426 | 150 |
else (i - text.length) max start |
34286 | 151 |
|
43425 | 152 |
def convert(i: Offset): Offset = transform(is_insert, i) |
153 |
def revert(i: Offset): Offset = transform(!is_insert, i) |
|
154 |
def convert(range: Range): Range = range.map(convert) |
|
155 |
def revert(range: Range): Range = range.map(revert) |
|
38425 | 156 |
|
34286 | 157 |
|
38425 | 158 |
/* edit strings */ |
159 |
||
38426 | 160 |
private def insert(i: Offset, string: String): String = |
161 |
string.substring(0, i) + text + string.substring(i) |
|
34276 | 162 |
|
38426 | 163 |
private def remove(i: Offset, count: Int, string: String): String = |
164 |
string.substring(0, i) + string.substring(i + count) |
|
38425 | 165 |
|
166 |
def can_edit(string: String, shift: Int): Boolean = |
|
167 |
shift <= start && start < shift + string.length |
|
168 |
||
169 |
def edit(string: String, shift: Int): (Option[Edit], String) = |
|
170 |
if (!can_edit(string, shift)) (Some(this), string) |
|
171 |
else if (is_insert) (None, insert(start - shift, string)) |
|
172 |
else { |
|
38426 | 173 |
val i = start - shift |
174 |
val count = text.length min (string.length - i) |
|
38425 | 175 |
val rest = |
176 |
if (count == text.length) None |
|
177 |
else Some(Edit.remove(start, text.substring(count))) |
|
38426 | 178 |
(rest, remove(i, count, string)) |
38425 | 179 |
} |
180 |
} |
|
34276 | 181 |
} |