Wait. We usually use "::", but sometimes we use \colcol, for no apparent reason. Ah, \colcol allows line breaks before and after the "::", which plain "::" doesn't.

But we have lots of places where we use ::\brk{}, not \colcol. Let's move that harmonizing discussion to a separate issue -> #1359.

The patch as proposed looks good to me.

This seems like churn. I'd say if you want to make progress here, replace the \colcol with plain double colons while you're at it.

Looks good, thanks. Can you just check quickly that this doesn't introduce any paragraph composition problems (overlong lines)? (E.g. by comparing the output of fgrep std.log -e Overfull -e .tex before and after.)

No. The output is the same before and after.

Thanks!