HomeIsabelle/Phabricator

document markers are formal comments, and may thus occur anywhere in theā€¦

Description

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;

Details

Provenance
makariusAuthored on
Parents
rISABELLEcb643a1a5313: PIDE markup for spell-checking;
Branches
Unknown
Tags
Unknown