On Sat, 24 Oct 2015, Tobias Nipkow wrote:
I don't know if this is related, but it must have happened recently: The
[display] option for antiquotations now (eg 436b7fe89cdc) generates latex
that indents the text following the display, even if there is no newline in
between. This is in contrast to latex conventions (eg \[ \]) and I would
rather not have to insert lots of \nondent by hand.
There is indeed one \n too much, which may produce an unintended
paragraph in LaTeX.
I've changed that as follows:
changeset: 61516:8e3705d91cfa
tag: tip
user: wenzelm
date: Mon Oct 26 18:04:17 2015 +0100
summary: clarified Latex.environment (again, amending e16649b70107):
avoid additional paragraph, e.g. relevant for option [display];
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
