tuned messages;

do not highlight ignored command spans; tuned;

more explicit handling of document;

explicit markup for forked goals, as indicated by Goal.fork; accumulate pending forks within command state and hilight accordingly; Isabelle_Process: enforce future_terminal_proof, which gives some impression of non-linear/parallel checking;

avoid :\ which is not tail-recursive and tends to overflow the tiny JVM stack, which is not resizable at runtime;

define_state/new_state: provide state immediately, which is now lazy; more careful document editing: single execution future forces all entries, synchronous cancelation after update;

force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling; recovered some similarity to sequential version;

future result: retain plain Interrupt for vacuous group exceptions;

remove two examples, now that the definition of "fst" and "snd" has changed

merged