batch file to strip numbers from filename and pad to two digits

Question

I have a text file with a list of server names (servers.txt) that looks something like this:

server1 server2 server3

I have a feeling this can be done with the FOR command as I use that to perform an action on each name in the file, but I'm not quite sure how to use the delimiters to accomplish this.

for /F "tokens=*" %%G in (servers.txt) do (  
  SET machinenum = <magic here>
  ECHO %machinenum%
)

expected output

01 02 03

Answer 1

Here's how you would do it in your example. Make the token larger (1-8) for however many servers you have. If you don't know how many servers you'll have, it would be a lot easier to put each server on it's own line.

for /f "tokens=1-3 delims=server" %%a in ('type server.txt') do set machinenum=0%%a0%%b0%%c
echo %machinenum%

If this is an actual batch file, use the double %%. If it's from the command line, use a single %

Answer 2

You'll need to set ENABLEDELAYEDEXPANSION to make this work.

The padding with a zero is hard. You might try:

setlocal ENABLEDELAYEDEXPANSION
@echo off
    for %%a in (00 01 02 03 04 05 06 07 08 09) do (
    set machinenum=
        @set machinenum=%%a
        @echo !machinenum!
        )       

If the zero is not necessary, you get some flexibility (assuming 20 servers):

setlocal ENABLEDELAYEDEXPANSION
@echo off
    for /l %%a in (1,1,20) do (
    set machinenum=
        @set machinenum=%%a
        @echo !machinenum!
        )