[isabelle-dev] infix line breaking

[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 that (and many other infix-related cans of
worms):
https://www.mail-archive.com/isabelle-dev@mailbroy.informatik.tu-muenchen.de/msg07670.html

Changing arrangements from many decades ago always takes a bit longer
than expected, and one needs to try hard to get a result that is
significantly better than the status-quo. We have require 2 full release
cycles just to get the relative simple reform of (+) and (*) through
(with a fully convincing result).


>From my side, the following two reforms are on the top of the stack of
further moves:

  (1) eliminate most (or all) ASCII replacement syntax with the help of
the "isabelle update" tool, e.g. ":" vs. "\<in>"

  (2) get ==> out of the infix topic for most practical purposes, by
printing goal states in Isar notation (fixes/assumes/shows or
fix/assume/show or show/if/for).

For the coming release I merely see (1) happening really soon: the
"isabelle update" tool belongs to certain newly introduced
infrastructure that deserves proper consolidation. (It is time to start
thinking about which already open threads should be closed for the release.)


	Makarius