Filter to add decimal separators to long numbers

decimal.sed

#!/bin/sed -Ef
#
# Add a LaTeX thin space (\,) decimal separator to long digit sequences
#
# Diomidis Spinellis, October 2018
#
# Save this as a file and add it to your path, or run at as a one-liner:
# sed -E ':a;s/([0-9])([0-9]{3})([^0-9]|$)/\1\\,\2\3/g;ta'
#

:a
# Add a , after a digit followed by three digits followed by non-digit or EOL
s/([0-9])([0-9]{3})([^0-9]|$)/\1\\,\2\3/

# Try the replacement again if the replacement succeeded
ta