Add an option with a color type.

Colors can be specified as "none" for terminal's default color, as a name of
one of the eight standard colors of ISO/IEC 6429 "black", "red", "green", etc.,
as an RGB hexadecimal tripplet #RRGGBB for 24-bit TrueColor, or as an
integer from 0 to 255.  Integers 0 to 7 are the synonyms for the standard
colors.  Integers 8-15 are used for the so-called bright colors from the
aixterm extended 16-color palette.  Integers 16-255 are the indexes into xterm
extended 256-color palette (usually 6x6x6 cube plus gray ramp).  In
general, 256-color palette is terminal dependent and sometimes can be
changed with OSC 4 sequences, e.g. "\033]4;1;rgb:00/FF/00\033\\".

It is the responsibility of the user to verify that the terminal supports
the specified colors.

PATCH v5 changes: documentation fixed.
PATCH v6 changes: documentation fixed.
PATCH v7 changes: rebase onto master and fixes after review.
PATCH v8 changes: fixes after review.

gdb/python/python.c

@@ -36,6 +36,7 @@
 #include "run-on-main-thread.h"
 #include "observable.h"
 #include "build-id.h"
+#include "py-color.h"
 
 #if GDB_SELF_TEST
 #include "gdbsupport/selftest.h"
@@ -511,6 +512,12 @@ gdbpy_parameter_value (const setting &var)
 	return host_string_to_python_string (str).release ();
       }
 
+    case var_color:
+      {
+	const ui_file_style::color &color = var.get<ui_file_style::color> ();
+	return create_color_object (color).release ();
+      }
+
     case var_boolean:
       {
 	if (var.get<bool> ())