OK, the answer that I have and which works almost exactly as requested is actually surprisingly complex. You will use
xmacro to record and play back key strokes.
sudo apt-get install xmacro
Record a macro
xmacrorec2 > test.macro
Now press ESC (to record the "abort" key for recording), type whatever text you want to assign and press ESC again to stop the recording. The recorded macro is now in the file
test.macro; you can edit it with a text editor.
Test that macro works
cat test.macro | xmacroplay -d 0 $DISPLAY
(optional, recommended) Create a script with the above commands. Save it as macro.sh:
cat test.macro | xmacroplay -d 0 $DISPLAY > /dev/null 2>/dev/null
Make it executable:
chmod a+x macro.sh
A little problem remains. xmacro plays back the exact keystrokes, but if you define a shortcut, and run the script from the shortcut, the keys will be played before you release the shortcut key, as if you started typing without releasing the key. You need to prepend the following line to the test.macro file:
which will simulate the release of the F1 key.
Using keyboard preferences (you can access them through settings or by typing `gnome-control-center keyboard), create a new shortcut under "Custom shortcuts" and assign to it F1.
OK, but there is one more caveat: the F1 shortcut will now work in every application, not only the terminal. I don't know how to solve it; possibly, in the
macro.sh one would have to test what window has the focus first and check whether the identifier of this window is terminal.