On 10/01/18 21:46, Tobias Nipkow wrote:
>
> Having the operator on the new line in case
> of a break makes a lot of sense to me because it clearly how this line
> is connected with the previous one. [I seem to remember Lamport makes a
> similar point but it is not in his "How to write a proof".]
>
> How about a uniform change to "breaks line BEFORE operator"?
The Haskell community appears to have picked up a lot of such (slightly
odd) styles from Lamport. E.g. they put commas at the start of the line
instead of the end, which is typographically very strange.
I was educated by the original TeX Book, which in turn refers to the
top-quality mathematical typesetting from around 1900. Here the
operators and commas are in the traditional position: end of line.
Anayway, such changes (after so many years) belong to the category of
"Brownian" motion: no clear direction, danger of moving back and forth,
producing more heat than light.
Note that the deeper problem with infixes is actually the question how
to lay out a long chain _ + _ + _ + _ + _ + _ with nice line breaks,
avoiding stair-cases.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
