modernized construction of type bcontfun; base explicit theorems on Uniform_Limit.thy; added some lemmas

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;

updated package;

dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);

tuned;

support for caret handling and dynamic output;

more complete exception handling;

tuned;

tuned;

tuned colors;

apply multiple edits bottom-to-top as specified in the protocol definition (assuming canonical order);

tuned colors;

proper Map operations; re-init decorations after configuration change;

tuned colors according to Light+ and Dark+ themes;

tuned signature;

updated package;

merged

tuned colors according to Light+ and Dark+ themes;

suppress irrelevant markup for VSCode;

tuned colors;