gdb/python: extend gdb.write to support styled output

gdb/python: extend gdb.write to support styled output

It is already possible to produce styled output from Python by
converting the gdb.Style to its escape code sequence, and writing that
to the output stream.

But this commit adds an alternative option to the mix by extending the
existing gdb.write() function to accept a 'style' argument.  The value
of this argument can be 'None' to indicate no style change should be
performed, this is the default, and matches the existing behaviour.

Or the new 'style' argument can be a gdb.Style object, in which case
the specified style is applied only for the string passed to
gdb.write, after which the default style is re-applied.

Using gdb.write with a style object more closely matches how GDB
handles styling internally, and has the benefit that the user doesn't
need to remember to restore the default style when they are done.

Reviewed-By: Eli Zaretskii <eliz@gnu.org>
Approved-By: Tom Tromey <tom@tromey.com>