Given this file
$ cat foo.txt AAA 111 BBB 222 CCC 333
I would like to replace the first line after BBB with 999. I came up with this command
awk '/BBB/ {f=1; print; next} f {$1=999; f=0} 1' foo.txt
but I am curious to any shorter commands with either awk or sed.