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;