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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
