1 /* Title: Pure/PIDE/text_edit.scala |
|
2 Author: Fabian Immler, TU Munich |
|
3 Author: Makarius |
|
4 |
|
5 Basic edits on plain text. |
|
6 */ |
|
7 |
|
8 package isabelle |
|
9 |
|
10 |
|
11 class Text_Edit(val is_insert: Boolean, val start: Int, val text: String) |
|
12 { |
|
13 override def toString = |
|
14 (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" |
|
15 |
|
16 |
|
17 /* transform offsets */ |
|
18 |
|
19 private def transform(do_insert: Boolean, offset: Int): Int = |
|
20 if (offset < start) offset |
|
21 else if (is_insert == do_insert) offset + text.length |
|
22 else (offset - text.length) max start |
|
23 |
|
24 def convert(offset: Int): Int = transform(true, offset) |
|
25 def revert(offset: Int): Int = transform(false, offset) |
|
26 |
|
27 |
|
28 /* edit strings */ |
|
29 |
|
30 private def insert(index: Int, string: String): String = |
|
31 string.substring(0, index) + text + string.substring(index) |
|
32 |
|
33 private def remove(index: Int, count: Int, string: String): String = |
|
34 string.substring(0, index) + string.substring(index + count) |
|
35 |
|
36 def can_edit(string: String, shift: Int): Boolean = |
|
37 shift <= start && start < shift + string.length |
|
38 |
|
39 def edit(string: String, shift: Int): (Option[Text_Edit], String) = |
|
40 if (!can_edit(string, shift)) (Some(this), string) |
|
41 else if (is_insert) (None, insert(start - shift, string)) |
|
42 else { |
|
43 val index = start - shift |
|
44 val count = text.length min (string.length - index) |
|
45 val rest = |
|
46 if (count == text.length) None |
|
47 else Some(new Text_Edit(false, start, text.substring(count))) |
|
48 (rest, remove(index, count, string)) |
|
49 } |
|
50 } |
|
51 |
|