Since it turns out this really is just a text dump and not some container format with any rigidity, I ended up using simple Unix text processing tools to convert it into a normal .hex file:
sed -ne 's/^ *:/:/p'
Simply use any text editor to remove everything but the HEX lines (started by a colon character ":"). This is how to get a pure HEX file. Colon has to be the very first character on each row, so remove the leading spaces too.
Step 2 - use e.g. ASM80 Tools for HEX to BIN conversion to convert it to binary image.
What is the name of this file format,
Well, it's called Intel-Hex-Format :))
Or are you asking about the file the link points to (tinybasic-2.0.hex) ?
That's no file format. It's simply the recording of a (terminal) output (*1) while one has first dumped the symbol list followed by the the Intel-Hex file.
and what modern tools can I use to convert it into ...