proper PIDE markup for codegen arguments;

less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace; propagate flush from ML to Scala via special protocol message; more formal type Message_Channel.message;

tuned -- more uniform ML vs. Scala;

recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;

more timing;

more timing; tuned -- Execution.is_running always holds due to immediate start;

removed spurious headings

more (co)datatype documentation

avoid DUP error in local context

sketched documentation for new (co)datatype package