--- a/src/Pure/PIDE/text.scala Tue Mar 25 22:23:27 2025 +0100
+++ b/src/Pure/PIDE/text.scala Tue Mar 25 23:05:15 2025 +0100
@@ -137,8 +137,10 @@
/* editing */
object Edit {
- def insert(start: Offset, text: String): Edit = new Edit(true, start, text)
- def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
+ def make(is_insert: Boolean, start: Offset, text: String): Edit =
+ new Edit(is_insert, start, text)
+ def insert(start: Offset, text: String): Edit = make(true, start, text)
+ def remove(start: Offset, text: String): Edit = make(false, start, text)
def inserts(start: Offset, text: String): List[Edit] =
if (text == "") Nil else List(insert(start, text))
def removes(start: Offset, text: String): List[Edit] =