# HG changeset patch
# User wenzelm
# Date 1742940315 -3600
# Node ID fcc0f74ac08607846bcbb09e69d674ad85611481
# Parent  c597898ff51b48781d9525c3181966f9d1b61c4c
tuned signature;

diff -r c597898ff51b -r fcc0f74ac086 src/Pure/PIDE/text.scala
--- 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] =