diff options
| author | Jim Fehrle | 2020-01-18 17:34:54 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2020-02-24 18:40:16 -0800 |
| commit | 1e7317701b9fc525ca54b9f961b5801068d0f314 (patch) | |
| tree | e38bd054595d4dfbe4bffbffafa53409f44da35f /plugins/syntax/string_notation.ml | |
| parent | 8c192db25a2dc11dd4136ed1b3b1af9a3ac6a18e (diff) | |
Add OPTREF and INSERTALL editing operations
Show effect of edits to edited nt in PRINT
Add cmdv:: info to prodnCommands
Supporting code globally replaces a given "substring" in productions
with another. (Substring over doc_symbols, not over characters.)
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions