MaSh exporter can now export subsets of the facts, as consecutive ranges

avoid creating nested threads for MaSh -- this seems to cause thread creation failures for machines with dozens of cores (unclear yet if that's really the issue)

thread no timeout properly

proper escaping in file name

encode lemma name in file name

more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment; more tooltip options via Rendering;

prefer more official getMenuShortcutKeyMask, in deviation to traditional jEdit technique;

maintain subtree_elements for improved performance of cumulate operator;

more formal class Markup_Tree.Elements;

tuned command line;

merged

unified layout of defs

tuned;

clarified build_dialog command line;

explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;

updated README;