[isabelle-dev] infix line breaking

[Tobias Nipkow]

We had already discussed this and decided that for "=", "<=" etc it makes sense.

I find that the wrong associativity can be much more of a killer than where the 
infix op is placed.

Tobias

On 22/02/2019 17:20, Lawrence Paulson wrote:
> The pretty printing of infix operators looks pretty terrible in the presence of large terms.
> 
> I’d like to propose having infix operators breaking at the start of the line rather than at the end. Any thoughts?
> 
> Larry
> 
> inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0) {pp}) {} (nsphere 0) {} r
>                                         d =
>      hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
>       (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere 0) {nn}) {} r
>         (inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5581 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190222/f01ab6d8/attachment.bin>