ghost bullet via markup, which is painted as bar under text (normally space);

replace induction by hammer

merged

merged;

basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);

maintain integer indentation during formatting -- it needs to be implemented by repeated spaces eventually; always round block indentation upwards, to ensure that text moves visually to the right of the "hanging" part;

tuned;