[isabelle-dev] NEWS: op <infix> -> (<infix>)

[Makarius]

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