[isabelle-dev] infix line breaking

[Lawrence Paulson]

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))