Jonathan, could you improve the comments for the dedent function? You have a great understanding of the logic flow from your proof and it would be beneficial to document this to avoid future confusion.

Specifically, it should be clear that Clause 2 inherently handles equivalence for margin and indent and that Clause 4 will always complete with the break statement.