Thanks, that did the trick. Tobias
On 26/10/2015 18:16, Makarius wrote:
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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
