Summary
- proper edits;
- suppress vacuous messages;
- clarified modules;
- more explicit message type: allows body to become empty;
- clarified current_command: index refers to node content, negative index means first command;
- clarified caret offset; show output at end of file;
- tuned signature;
- discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
- tuned;
- misc tuning and simplification;
- misc tuning and simplification;