1/* Title: Pure/PIDE/text.scala 2 Author: Fabian Immler, TU Munich 3 Author: Makarius 4 5Basic operations on plain text. 6*/ 7 8package isabelle 9 10 11import scala.collection.mutable 12import scala.util.Sorting 13 14 15object Text 16{ 17 /* offset */ 18 19 type Offset = Int 20 21 22 /* range -- with total quasi-ordering */ 23 24 object Range 25 { 26 def apply(start: Offset): Range = Range(start, start) 27 28 val full: Range = apply(0, Integer.MAX_VALUE / 2) 29 val offside: Range = apply(-1) 30 31 object Ordering extends scala.math.Ordering[Range] 32 { 33 def compare(r1: Range, r2: Range): Int = r1 compare r2 34 } 35 } 36 37 sealed case class Range(start: Offset, stop: Offset) 38 { 39 // denotation: {start} Un {i. start < i & i < stop} 40 if (start > stop) 41 error("Bad range: [" + start.toString + ".." + stop.toString + "]") 42 43 override def toString: String = "[" + start.toString + ".." + stop.toString + "]" 44 45 def length: Offset = stop - start 46 47 def map(f: Offset => Offset): Range = Range(f(start), f(stop)) 48 def +(i: Offset): Range = if (i == 0) this else map(_ + i) 49 def -(i: Offset): Range = if (i == 0) this else map(_ - i) 50 51 def is_singularity: Boolean = start == stop 52 def inflate_singularity: Range = if (is_singularity) Range(start, start + 1) else this 53 54 def touches(i: Offset): Boolean = start <= i && i <= stop 55 56 def contains(i: Offset): Boolean = start == i || start < i && i < stop 57 def contains(that: Range): Boolean = this.contains(that.start) && that.stop <= this.stop 58 def overlaps(that: Range): Boolean = this.contains(that.start) || that.contains(this.start) 59 def compare(that: Range): Int = if (overlaps(that)) 0 else this.start compare that.start 60 61 def apart(that: Range): Boolean = 62 (this.start max that.start) > (this.stop min that.stop) 63 64 def restrict(that: Range): Range = 65 Range(this.start max that.start, this.stop min that.stop) 66 67 def try_restrict(that: Range): Option[Range] = 68 if (this apart that) None 69 else Some(restrict(that)) 70 71 def try_join(that: Range): Option[Range] = 72 if (this apart that) None 73 else Some(Range(this.start min that.start, this.stop max that.stop)) 74 75 def substring(text: String): String = text.substring(start, stop) 76 77 def try_substring(text: String): Option[String] = 78 try { Some(substring(text)) } 79 catch { case _: IndexOutOfBoundsException => None } 80 } 81 82 83 /* perspective */ 84 85 object Perspective 86 { 87 val empty: Perspective = Perspective(Nil) 88 89 def full: Perspective = Perspective(List(Range.full)) 90 91 def apply(ranges: List[Range]): Perspective = 92 { 93 val result = new mutable.ListBuffer[Range] 94 var last: Option[Range] = None 95 def ship(next: Option[Range]) { result ++= last; last = next } 96 97 for (range <- ranges.sortBy(_.start)) 98 { 99 last match { 100 case None => ship(Some(range)) 101 case Some(last_range) => 102 last_range.try_join(range) match { 103 case None => ship(Some(range)) 104 case joined => last = joined 105 } 106 } 107 } 108 ship(None) 109 new Perspective(result.toList) 110 } 111 } 112 113 final class Perspective private( 114 val ranges: List[Range]) // visible text partitioning in canonical order 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) 120 121 override def hashCode: Int = ranges.hashCode 122 override def equals(that: Any): Boolean = 123 that match { 124 case other: Perspective => ranges == other.ranges 125 case _ => false 126 } 127 override def toString: String = ranges.toString 128 } 129 130 131 /* information associated with text range */ 132 133 sealed case class Info[A](range: Range, info: A) 134 { 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)) 137 138 def map[B](f: A => B): Info[B] = Info(range, f(info)) 139 } 140 141 type Markup = Info[XML.Elem] 142 143 144 /* editing */ 145 146 object Edit 147 { 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) 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)) 154 def replace(start: Offset, old_text: String, new_text: String): List[Edit] = 155 if (old_text == new_text) Nil 156 else removes(start, old_text) ::: inserts(start, new_text) 157 } 158 159 final class Edit private(val is_insert: Boolean, val start: Offset, val text: String) 160 { 161 override def toString: String = 162 (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" 163 164 165 /* transform offsets */ 166 167 private def transform(do_insert: Boolean, i: Offset): Offset = 168 if (i < start) i 169 else if (do_insert) i + text.length 170 else (i - text.length) max start 171 172 def convert(i: Offset): Offset = transform(is_insert, i) 173 def revert(i: Offset): Offset = transform(!is_insert, i) 174 175 176 /* edit strings */ 177 178 private def insert(i: Offset, string: String): String = 179 string.substring(0, i) + text + string.substring(i) 180 181 private def remove(i: Offset, count: Offset, string: String): String = 182 string.substring(0, i) + string.substring(i + count) 183 184 def can_edit(string: String, shift: Offset): Boolean = 185 shift <= start && start < shift + string.length 186 187 def edit(string: String, shift: Offset): (Option[Edit], String) = 188 if (!can_edit(string, shift)) (Some(this), string) 189 else if (is_insert) (None, insert(start - shift, string)) 190 else { 191 val i = start - shift 192 val count = text.length min (string.length - i) 193 val rest = 194 if (count == text.length) None 195 else Some(Edit.remove(start, text.substring(count))) 196 (rest, remove(i, count, string)) 197 } 198 } 199} 200