Text Escaping

[justinpombrio]

In a JSON string:

• " inserts a quote, displayed as ", represented as \", printed as \", treated as a single char in text navigation.
• \ opens a menu, \n inserts a newline, displayed as \n, represented as \n, printed as \n, treated as a single char in text navigation.

This can be accomplished by having a replacement table, mapping a "source string" to a "display string". Then:

• Texty construct has an optional replacement table.
• Text has a source string and an optional display string.
• Location::InText has an index into the source string.
• When printing to source, unwrap_text returns a reference to the source string.
• When displaying, unwrap_text returns a reference to the display string (fallback to the source string, implying that they're equal).
• path_to_root() converts the source text index into a display text index if needed.
• Text navigation and editing commands check the replacement table, treating each entry like a single char. They update both the source and display strings in sync.