document-style default: "book" A string describing the document style.
user-style default: #f A string denoting a the name of a file
specifying user customization
font-type default: "roman" A string denoting the default font family.
font-size default: 11 An integer representing the default font size.
image-format default: ("jpg") A list of supported image formats.
source-comment-color default: "#ffa600" The source comment color.
source-error-color default: "red" The source error color.
source-define-color default: "#6959cf" The source define color.
source-module-color default: "#1919af" The source module color.
source-markup-color default: "#1919af" The source markup color.
source-thread-color default: "#ad4386" The source thread color.
source-string-color default: "red" The source string color.
source-bracket-color default: "red" The source bracket color.
source-type-color default: "#00cf00" The source type color.