On Thursday, July 13, 2023 at 11:53:17 AM UTC-5 Edward K. Ream wrote: > Otoh, undoing an accidental abbreviation is essential.
Happily, the existing code handles non-tree abbreviations. Fully undoing a tree abbreviation would be harder. Happily, it's not necessary. Undo *does* work just as with non-tree abbreviations, but the inserted tree remains. The user can easily delete the tree. Edward -- You received this message because you are subscribed to the Google Groups "leo-editor" group. To unsubscribe from this group and stop receiving emails from it, send an email to leo-editor+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/leo-editor/54771721-3f11-4840-9aa4-24cc7a892be0n%40googlegroups.com.
