When the user wants to undo a certain type of formatting operation, the formatting record can be used to easily understand what parameters to add to cancel the formatting operation.
Records content such like:
-- if a==b
++ if a == b -- set no_add_space to disable this formatting
When the user wants to undo a certain type of formatting operation, the formatting record can be used to easily understand what parameters to add to cancel the formatting operation.
Records content such like: