/* Ciao syntax */
span.ciao-face-sectioning-5-face   { color: #000080; font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; text-decoration: none; }
span.ciao-face-sectioning-5-face a { color: #000080; font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; text-decoration: underline; }
span.ciao-face-sectioning-4-face   { color: #000080; font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; font-size: 15pt; text-decoration: none; }
span.ciao-face-sectioning-4-face a { color: #000080; font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; font-size: 15pt; text-decoration: underline; }
span.ciao-face-sectioning-3-face   { color: #000080; font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; font-size: 18pt; text-decoration: none; }
span.ciao-face-sectioning-3-face a { color: #000080; font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; font-size: 18pt; text-decoration: underline; }
span.ciao-face-sectioning-2-face   { color: #000080; font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; font-size: 20pt; text-decoration: none; }
span.ciao-face-sectioning-2-face a { color: #000080; font-weight: 700; font-family: "Trebuchet MS", Helvetica, sans-serif; font-size: 20pt; text-decoration: underline; }
span.ciao-face-funexp-atom   { color: #6b8e23; font-weight: 500; text-decoration: none; }
span.ciao-face-funexp-atom a { color: #6b8e23; font-weight: 500; text-decoration: underline; }
span.ciao-face-type-assrt   { color: #0000cd; font-weight: 700; text-decoration: none; }
span.ciao-face-type-assrt a { color: #0000cd; font-weight: 700; text-decoration: underline; }
span.ciao-face-prop-assrt   { color: #0000ff; font-weight: 700; text-decoration: none; }
span.ciao-face-prop-assrt a { color: #0000ff; font-weight: 700; text-decoration: underline; }
span.ciao-face-entry-assrt   { color: #a52a2a; font-weight: 700; text-decoration: none; }
span.ciao-face-entry-assrt a { color: #a52a2a; font-weight: 700; text-decoration: underline; }
span.ciao-face-trust-assrt   { color: #ff7f50; font-weight: 700; text-decoration: none; }
span.ciao-face-trust-assrt a { color: #ff7f50; font-weight: 700; text-decoration: underline; }
span.ciao-face-false-assrt   { color: #ff0000; font-weight: 700; text-decoration: none; }
span.ciao-face-false-assrt a { color: #ff0000; font-weight: 700; text-decoration: underline; }
span.ciao-face-true-assrt   { color: #228b22; font-weight: 700; text-decoration: none; }
span.ciao-face-true-assrt a { color: #228b22; font-weight: 700; text-decoration: underline; }
span.ciao-face-check-assrt   { color: #000080; font-weight: 700; text-decoration: none; }
span.ciao-face-check-assrt a { color: #000080; font-weight: 700; text-decoration: underline; }
span.ciao-face-checked-assrt   { color: #006400; font-weight: 700; text-decoration: none; }
span.ciao-face-checked-assrt a { color: #006400; font-weight: 700; text-decoration: underline; }
span.ciao-face-lpdoc-command   { color: #4169e1; font-weight: 500; text-decoration: none; }
span.ciao-face-lpdoc-command a { color: #4169e1; font-weight: 500; text-decoration: underline; }
span.ciao-face-lpdoc-verbatim   { color: #000080; font-weight: 700; text-decoration: none; }
span.ciao-face-lpdoc-verbatim a { color: #000080; font-weight: 700; text-decoration: underline; }
span.ciao-face-lpdoc-include   { color: #000080; font-weight: 700; text-decoration: none; }
span.ciao-face-lpdoc-include a { color: #000080; font-weight: 700; text-decoration: underline; }
span.ciao-face-concurrency-op   { color: #ff7f50; font-weight: 700; text-decoration: none; }
span.ciao-face-concurrency-op a { color: #ff7f50; font-weight: 700; text-decoration: underline; }
span.ciao-face-prompt   { color: #ff7f50; font-weight: 700; text-decoration: none; }
span.ciao-face-prompt a { color: #ff7f50; font-weight: 700; text-decoration: underline; }
span.ciao-face-variable   { color: #a0522d; font-weight: 500; text-decoration: none; }
span.ciao-face-variable a { color: #a0522d; font-weight: 500; text-decoration: underline; }
span.ciao-face-string   { color: #bc8f8f; font-weight: 500; text-decoration: none; }
span.ciao-face-string a { color: #bc8f8f; font-weight: 500; text-decoration: underline; }
span.ciao-face-lpdoc-comment   { color: #000080; font-weight: 500; text-decoration: none; }
span.ciao-face-lpdoc-comment a { color: #000080; font-weight: 500; text-decoration: underline; }
span.ciao-face-lpdoc-bug-comment   { color: #ff0000; font-weight: 700; text-decoration: none; }
span.ciao-face-lpdoc-bug-comment a { color: #ff0000; font-weight: 700; text-decoration: underline; }
span.ciao-face-clauseheadname   { color: #0000ff; font-weight: 500; text-decoration: none; }
span.ciao-face-clauseheadname a { color: #0000ff; font-weight: 500; text-decoration: underline; }
span.ciao-face-user-directive   { color: #000080; font-weight: 500; text-decoration: none; }
span.ciao-face-user-directive a { color: #000080; font-weight: 500; text-decoration: underline; }
span.ciao-face-library-directive   { color: #000080; font-weight: 700; text-decoration: none; }
span.ciao-face-library-directive a { color: #000080; font-weight: 700; text-decoration: underline; }
span.ciao-face-predicate-directive   { color: #4169e1; font-weight: 500; text-decoration: none; }
span.ciao-face-predicate-directive a { color: #4169e1; font-weight: 500; text-decoration: underline; }
span.ciao-face-builtin-directive   { color: #0000ff; font-weight: 700; text-decoration: none; }
span.ciao-face-builtin-directive a { color: #0000ff; font-weight: 700; text-decoration: underline; }
span.ciao-face-quoted-atom   { color: #666666; font-weight: 500; text-decoration: none; }
span.ciao-face-quoted-atom a { color: #666666; font-weight: 500; text-decoration: underline; }
span.ciao-face-module-directive   { color: #000080; font-weight: 700; text-decoration: none; }
span.ciao-face-module-directive a { color: #000080; font-weight: 700; text-decoration: underline; }
span.ciao-face-comment   { color: #b22222; font-weight: 500; text-decoration: none; }
span.ciao-face-comment a { color: #b22222; font-weight: 500; text-decoration: underline; }
span.ciao-face-cut   { color: #4169e1; font-weight: 500; text-decoration: none; }
span.ciao-face-cut a { color: #4169e1; font-weight: 500; text-decoration: underline; }
/* Other languages */
span.constant   { color: #008b8b; font-weight: 500; text-decoration: none; }
span.constant a { color: #008b8b; font-weight: 500; text-decoration: underline; }
span.negation-char   { font-weight: 500; color: #000000; text-decoration: none; }
span.negation-char a { font-weight: 500; color: #000000; text-decoration: underline; }
span.variable-name   { color: #a0522d; font-weight: 500; text-decoration: none; }
span.variable-name a { color: #a0522d; font-weight: 500; text-decoration: underline; }
span.type   { color: #228b22; font-weight: 500; text-decoration: none; }
span.type a { color: #228b22; font-weight: 500; text-decoration: underline; }
span.hc-tab   { background: #000000; font-weight: 500; color: #000000; text-decoration: none; }
span.hc-tab a { background: #000000; font-weight: 500; color: #000000; text-decoration: underline; }
span.hc-trailing-whitespace   { background: #000000; font-weight: 500; color: #000000; text-decoration: none; }
span.hc-trailing-whitespace a { background: #000000; font-weight: 500; color: #000000; text-decoration: underline; }
span.function-name   { color: #0000ff; font-weight: 500; text-decoration: none; }
span.function-name a { color: #0000ff; font-weight: 500; text-decoration: underline; }
span.keyword   { color: #a020f0; font-weight: 500; text-decoration: none; }
span.keyword a { color: #a020f0; font-weight: 500; text-decoration: underline; }
span.string   { color: #8b2252; font-weight: 500; text-decoration: none; }
span.string a { color: #8b2252; font-weight: 500; text-decoration: underline; }
span.preprocessor   { color: #483d8b; font-weight: 500; text-decoration: none; }
span.preprocessor a { color: #483d8b; font-weight: 500; text-decoration: underline; }
span.comment   { color: #b22222; font-weight: 500; text-decoration: none; }
span.comment a { color: #b22222; font-weight: 500; text-decoration: underline; }
span.comment-delimiter   { color: #b22222; font-weight: 500; text-decoration: none; }
span.comment-delimiter a { color: #b22222; font-weight: 500; text-decoration: underline; }
span.sh-quoted-exec   { color: #ff00ff; font-weight: 500; text-decoration: none; }
span.sh-quoted-exec a { color: #ff00ff; font-weight: 500; text-decoration: underline; }