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