[isabelle-dev] infix line breaking

[Lawrence Paulson]

The point is the line breaking. Look at the occurrence of d before the =. This applies to all infix operators, not just relations.
Larry

> On 22 Feb 2019, at 17:10, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev