[isabelle-dev] NEWS: op <infix> -> (<infix>)
nipkow at in.tum.de
Wed Jan 10 21:46:20 CET 2018
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 eab6ce8368fa
> These 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
> 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"?
> 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.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
More information about the isabelle-dev