more position information;

tuned;

support to encode/decode command state;
support to merge full contents of command state;

support for context block structure in Sidekick;
tuned;

misc tuning and simplification;

clarified span position;

simplified Command.resolve_files in ML, using blobs_index from Scala;
clarified modules;

clarified command content;

tuned -- more uniform ML vs. Scala;

find command span in buffer;
tuned signature;

maintain Command_Range position as in ML;

separate module Command_Span: mostly syntactic representation;
potentially prover-specific Output_Syntax.parse_spans;