[isabelle-dev] NEWS: op <infix> -> (<infix>)

[Tobias Nipkow]

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
> 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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5156 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180110/e7c6ae12/attachment.bin>