Re: [isabelle-dev] infix line breaking

2019-02-22 Thread 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 wrote: > > We had already discussed this and decided that for "=", "<=" etc it makes > sense. > > I find that the

[isabelle-dev] infix line breaking

2019-02-22 Thread 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})

Re: [isabelle-dev] infix line breaking

2019-02-22 Thread 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

[isabelle-dev] Wrong position information in 3bfa28b3a5b2

2019-02-22 Thread Manuel Eberl
I came upon a regrssion with the position information in terms that contain calligraphic or Fraktur letters, e.g.: theory Scratch   imports Pure begin lemma "풜 풜 풜 풜 ()) a b c d e" The syntax error in this line is at the second closing parenthesis. In 3bfa28b3a5b2, Isabelle/jEdit displays the

Re: [isabelle-dev] infix line breaking

2019-02-22 Thread Makarius
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? Recall this recent thread on

Re: [isabelle-dev] Wrong position information in 3bfa28b3a5b2

2019-02-22 Thread Makarius
On 22/02/2019 16:47, Manuel Eberl wrote: > I came upon a regrssion with the position information in terms that > contain calligraphic or Fraktur letters, e.g.: > > theory Scratch >   imports Pure > begin > > lemma "풜 풜 풜 풜 ()) a b c d e" > > The syntax error in this line is at the second