@@ -143,15 +143,15 @@ Produces a diff that splits either on characters, tokens, or not at all, dependi
143143Guarantees that all actions in the output will be maximally grouped; that is, instead of returning
144144`#[(.insert, "a"), (.insert, "b")]`, it will return `#[(.insert, "ab")]`.
145145-/
146- partial def readableDiff (s s' : String) (granularity : DiffGranularity) : Array (Diff.Action × String) :=
146+ partial def readableDiff (s s' : String) (granularity : DiffGranularity := .auto ) : Array (Diff.Action × String) :=
147147 match granularity with
148148 | .char => charDiff
149149 | .word => wordDiff
150150 | .all => maxDiff
151151 | .auto =>
152152 let minLength := min s.length s'.length
153153 -- The coefficients on these values can be tuned:
154- let maxCharDiffDistance := minLength / 2
154+ let maxCharDiffDistance := minLength / 5
155155 let maxWordDiffDistance := minLength / 2 + (max s.length s'.length) / 2
156156
157157 let charDiffRaw := Diff.diff (splitChars s) (splitChars s')
@@ -175,12 +175,13 @@ where
175175 whitespace and accurately previewing what will be inserted. We err on the side of the latter.
176176 Within a "run" of deletions or insertions, we maintain the whitespace from the deleted/inserted
177177 text and mark it as a deletion/insertion. After an unchanged word or a substitution (i.e., a
178- deletion and insertion without an intervening unchanged word), we use the whitespace from the
179- new version but mark it as unchanged, since there was also whitespace (of some possibly different
180- form) here originally too. Within a substitution, we omit whitespace entirely. After an insertion,
181- we show the new whitespace but mark it as an insertion; after a deletion, we render the old
182- whitespace as a deletion unless it contains a newline, in which case it is omitted (as rendering a
183- deleted newline still visually suggests a line break in the new output).
178+ deletion and insertion without an intervening unchanged word), we show a whitespace diff iff the
179+ old whitespace did not contain a line break (as rendering a deleted newline still visually
180+ suggests a line break in the new output); otherwise, we use the whitespace from the new version
181+ but mark it as unchanged, since there was also whitespace here originally too. Within a
182+ substitution, we omit whitespace entirely. After an insertion, we show the new whitespace and mark
183+ it as an insertion. After a deletion, we render the old whitespace as a deletion unless it
184+ contains a newline, for the same reason mentioned previously.
184185 -/
185186 wordDiff := Id.run do
186187 let (words, wss) := splitWords s
@@ -195,33 +196,41 @@ where
195196 if let some (a₂, s₂) := diff[diffIdx + 1 ]? then
196197 match a₁, a₂ with
197198 | .skip, .delete =>
198- -- Unchanged word: use new whitespace unless this is followed by a deleted terminal
199- -- substring of the old, in which case use the old whitespace
200- if let some ws := wss'[wss'Idx]? then
201- withWs := withWs.push (.skip, ws)
199+ -- Unchanged word: show whitespace diff unless this is followed by a deleted terminal
200+ -- substring of the old, in which case show the old whitespace (since there is no new)
201+ let ws := wss[wssIdx]!
202+ let wsDiff := if let some ws' := wss'[wss'Idx]? then
203+ mkWhitespaceDiff ws ws'
202204 else
203- let ws := wss[wssIdx]!
204- withWs := withWs.push (.delete, ws)
205+ #[(.delete, ws)]
206+ withWs := withWs ++ wsDiff
205207 wssIdx := wssIdx + 1
206208 wss'Idx := wss'Idx + 1
207209 | .skip, .skip | .skip, .insert =>
208- -- Unchanged word: new has white space here (use it); old does too so long as we haven't
209- -- reached an appended terminal new portion
210- let ws := wss'[wss'Idx]!
211- withWs := withWs.push (.skip, ws)
210+ -- Unchanged word: inverse of the above case: new has whitespace here, and old does too so
211+ -- long as we haven't reached an appended terminal new portion
212+ let ws' := wss'[wss'Idx]!
213+ let wsDiff := if let some ws := wss[wssIdx]? then
214+ mkWhitespaceDiff ws ws'
215+ else
216+ #[(.insert, ws')]
217+ withWs := withWs ++ wsDiff
212218 wssIdx := wssIdx + 1
213219 wss'Idx := wss'Idx + 1
214220 | .insert, .insert =>
215- -- Insertion separator: include, and mark it as inserted
221+ -- Insertion separator: include whitespace , and mark it as inserted
216222 let ws := wss'[wss'Idx]!
217223 withWs := withWs.push (.insert, ws)
218224 wss'Idx := wss'Idx + 1
219225 | .insert, .skip =>
220- -- End of insertion: if this was a substitution, new and old have whitespace here, and we
221- -- take the new one; if it wasn't, only new has whitespace here
222- let ws := wss'[wss'Idx]!
223- let act := if inSubst then .skip else .insert
224- withWs := withWs.push (act, ws)
226+ -- End of insertion: if this was a substitution, new and old have whitespace here; if it
227+ -- wasn't, only new has whitespace here
228+ let ws' := wss'[wss'Idx]!
229+ let wsDiff := if inSubst then
230+ mkWhitespaceDiff wss[wssIdx]! ws'
231+ else
232+ #[(.insert, ws')]
233+ withWs := withWs ++ wsDiff
225234 wss'Idx := wss'Idx + 1
226235 if inSubst then wssIdx := wssIdx + 1
227236 inSubst := false
@@ -248,13 +257,21 @@ where
248257 |>.map fun (act, ss) => (act, ss.foldl (· ++ ·) "" )
249258
250259 charDiff :=
251- Diff.diff (splitChars s) (splitChars s')
252- |> joinEdits
253- |>.map fun (act, cs) => (act, String.mk cs.toList)
260+ Diff.diff (splitChars s) (splitChars s') |> joinCharDiff
261+
262+ /-- Given a `Char` diff, produces an equivalent `String` diff, joining actions of the same kind. -/
263+ joinCharDiff (d : Array (Diff.Action × Char)) :=
264+ joinEdits d |>.map fun (act, cs) => (act, String.mk cs.toList)
254265
255266 maxDiff :=
256267 #[(.delete, s), (.insert, s')]
257268
269+ mkWhitespaceDiff (oldWs newWs : String) :=
270+ if !oldWs.contains '\n ' then
271+ Diff.diff oldWs.data.toArray newWs.data.toArray |> joinCharDiff
272+ else
273+ #[(.skip, newWs)]
274+
258275 splitChars (s : String) : Array Char :=
259276 s.toList.toArray
260277
0 commit comments