On 10/01/2018 21:23, Makarius wrote:
On 10/01/18 20:17, Tobias Nipkow wrote:Invoking "isabelle update_op" converts all files in the current directory (recursively). In case you want to exclude conversion of ML files (because the tool frequently also converts ML's "op" syntax), use option "-m". In revision eab6ce8368faThese are more changes than I expected, but even that is to be expected with the wealth of material we have accumulated :-) BTW, in the follow-up change a82df75b7f85 ("tuned notation") the special breaks introduced by Larry in 1996 got lost: changeset: 2006:72754e060aa2 user: paulson date: Mon Sep 23 17:47:49 1996 +0200 files: src/HOL/Ord.thy src/HOL/Set.thy description: New infix syntax: breaks line BEFORE operator
I did wonder if it had been done on purpose and toyed with the idea of consulting the history but the "uniformity" drive won. Thanks for keeping me honest. But I do wonder: shouldn't all infix operators be printed in the same manner? Having the operator on the new line in case of a break makes a lot of sense to me because it clearly how this line is connected with the previous one. [I seem to remember Lamport makes a similar point but it is not in his "How to write a proof".]
How about a uniform change to "breaks line BEFORE operator"? Tobias
Larry has recently done analogous changes (e.g. bdf25939a550), so it
appears to be still the state-of-the art to have these exceptions in
pretty printing.
Makarius
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
