refactor: start_modify → inserted

src/Lean/Widget/Diff.lean

@@ -45,17 +45,18 @@ partial def isParent (m₁ m₂ : MVarId) : MetaM Bool := do
   )
   return r.isSome
 
+/-- A marker for a point in the expression where a subexpression has been inserted.
+
+NOTE: in the future it may make sense to add `deleted` or `end_insert` tags too.
+  -/
 inductive ExprDiffPoint where
-  | start_modify
-  | end_modify
+  | inserted
 
 def ExprDiffPoint.toString : ExprDiffPoint → String
-  | .start_modify => "start_modify"
-  | .end_modify => "end_modify"
+  | .inserted => "inserted"
 
 def ExprDiffPoint.fromString : String → Except String ExprDiffPoint
-  | "start_modify" => Except.ok ExprDiffPoint.start_modify
-  | "end_modify" => Except.ok ExprDiffPoint.end_modify
+  | "inserted" => Except.ok ExprDiffPoint.inserted
   | s => Except.error s!"expected an ExprDiffPoint ctor string but got {s}"
 
 instance : FromJson ExprDiffPoint where
@@ -89,23 +90,23 @@ def sameHead (e₀ e₁ : Expr) : MetaM Bool := do
 def ExprDiff.isRootReplacement (d : ExprDiff) : MetaM Bool := do
   if d.isEmpty then return false else
   match d.changes.find? Pos.root with
-  | (some .start_modify) => return true
+  | (some .inserted) => return true
   | _ => return false
 
 partial def exprDiff (before after : Expr) (p : Pos := Pos.root) : MetaM ExprDiff := do
   if before == after then
     return ∅
   if !(← sameHead before after) then
-    return ExprDiff.tell p ExprDiffPoint.start_modify
+    return ExprDiff.tell p ExprDiffPoint.inserted
   let afterArgs := after.getAppArgs
   let beforeArgs := before.getAppArgs
   if afterArgs.size == 0 then
-    return ExprDiff.tell p ExprDiffPoint.start_modify
+    return ExprDiff.tell p ExprDiffPoint.inserted
   let n := afterArgs.size
   let bas := Array.zip beforeArgs afterArgs
   let numDifferent := bas.filter (fun (a,b) => a != b) |>.size
   if numDifferent > 1 ∧ p != Pos.root then
-    return ExprDiff.tell p ExprDiffPoint.start_modify
+    return ExprDiff.tell p ExprDiffPoint.inserted
   let rs : Array ExprDiff ← bas.mapIdxM (fun i (x,y) => do
     exprDiff x y <| p.pushNaryArg n i
   )