inline markup for Output.state (in contrast to c94bba7906d2): make messages available via Rendering.text_messages and thus "isabelle log" (see cb0c407fbc6e), while Rendering.output_messages of Isabelle/jEdit/VSCode is unaffected;

proper antiquotations;

clarified options, following e.g. "show_consts";

proper Envir.subst operations: env is already normalized, using Envir.norm may lead to non-termination;

unused (see 15758fced053);

clarified modules;

show goal instantiation, notably for 'schematic_goal' command (inactive by default);

proper umlauts;

tuned signature;

tuned signature;