Lean4
/-- `mkWindow orig start ctx` extracts from `orig` a string that starts at the first
non-whitespace character before `start`, then expands to cover `ctx` more characters
and continues still until the first non-whitespace character.
In essence, it extracts the substring of `orig` that begins at `start`, continues for `ctx`
characters plus expands left and right until it encounters the first whitespace character,
to avoid cutting into "words".
*Note*. `start` is the number of characters *from the right* where our focus is!
-/
def mkWindow (orig : String) (start ctx : Nat) : String :=
let head :=
orig.dropRight
(start + 1) -- `orig`, up to one character before the discrepancy
let middle := orig.takeRight (start + 1)
let headCtx := head.takeRightWhile (!·.isWhitespace)
let tail := middle.drop ctx |>.takeWhile (!·.isWhitespace)
s! "{headCtx}{(middle.take ctx)}{tail}"
