document markers are formal comments, and may thus occur anywhere in the command-span;
clarified Outer_Syntax.parse_span, Outer_Syntax.parse_text wrt. span structure;
tuned signature;
Description
Description
Details
Details
- Provenance
makarius Authored on - Parents
- rISABELLEcb643a1a5313: PIDE markup for spell-checking;
- Branches
- Unknown
- Tags