A:link {color: #0000DD} A:visited {color: #551188} A:hover {color: #3333FF} A:active {color: #FF00FF} A * {text-decoration: inherit} .title1 {font-family: "Times New Roman", Times, serif; font-size: 36pt; font-weight: bold; color: #000000; white-space: nowrap} .title2 {font-family: "Times New Roman", Times, serif; font-size: 18pt; font-weight: bold; color: #000000; white-space: nowrap} .top-title {color: #009900} .es-title {color: #999900} .draft-title {color: #FF0000} .mod-date {font-size: smaller; font-style: italic; text-align: right} .syntax {margin-left: 36pt} .indent {margin-left: 36pt} .issue {color: #FF0000} .small-caps {font-variant: small-caps} BODY {background-color: #FFFFFF; color: #000000} DL {margin-left: 18pt} DD {margin-bottom: 6pt} DT {font-style: italic; margin-top: 3pt} .js2 {background-color: #FFFF66; color: #000033} .js2-hidden {} .es4 {background-color: #FFCCCC; color: #333300; text-decoration: line-through} .es4-hidden {} .grammar-rule {margin-left: 18pt; margin-top: 6pt; margin-bottom: 6pt} .grammar-lhs {} .grammar-rhs {margin-left: 9pt;} .grammar-argument {margin-left: 18pt; margin-top: 6pt; margin-bottom: 6pt} .semantic-comment {margin-left: 9pt; margin-top: 9pt; margin-bottom: 0pt} .stmt {margin-left: 36pt; text-indent: -36pt} .lvl {margin-left: 18pt} .lvl-wide {margin-left: 18pt; margin-bottom: 6pt} .algorithm {margin-left: 9pt; margin-top: 6pt; margin-bottom: 6pt} .algorithm-indent {margin-left: 36pt; margin-top: 6pt; margin-bottom: 6pt} .algorithm-stmt {margin-left: 45pt; text-indent: -36pt; margin-top: 6pt; margin-bottom: 6pt} .symbol {font-family: Symbol} .unicode {font-family: "Lucida Sans Unicode", serif} VAR, VAR A:link, VAR A:visited {font-family: Georgia, Palatino, "Times New Roman", Times, serif; font-weight: normal; font-style: italic; color: #336600} A:hover VAR, VAR A:hover {color: #003300} A:active VAR, VAR A:active {color: #00FF00} .var-sub {color: #336600} CODE, PRE {font-family: "Courier New", Courier, mono; color: #0000FF} PRE {margin-left: 36pt} A:hover CODE {color: #3333CC} A:active CODE {color: #6666FF} .control, A.control:link, A.control:visited {font-family: "Times New Roman", Times, serif; font-weight: normal; color: #000099} A.control:hover, A:hover .control {color: #333366} A.control:active, A:active .control {color: #3333FF} .terminal, A.terminal:link, A.terminal:visited {font-family: Georgia, Palatino, "Times New Roman", Times, serif; font-weight: bold; color: #009999} A.terminal:hover, A:hover .terminal {color: #336666} A.terminal:active, A:active .terminal {color: #00FFFF} .terminal-keyword {font-weight: bold} .terminal-sub {color: #009999} .nonterminal, A.nonterminal:link, A.nonterminal:visited, .nonterminal A:link, .nonterminal A:visited {font-family: Georgia, Palatino, "Times New Roman", Times, serif; font-weight: normal; font-style: italic; color: #009900} A.nonterminal:hover, .nonterminal A:hover, A:hover .nonterminal {color: #336633} A.nonterminal:active, .nonterminal A:active, A:active .nonterminal {color: #00FF00} .nonterminal-attribute {font-family: Arial, Helvetica, sans-serif; color: #009900} .nonterminal-argument {color: #009900} .nonterminal-sub {color: #009900} .semantic-keyword {font-family: "Times New Roman", Times, serif; font-weight: bold} .domain-name, A.domain-name:link, A.domain-name:visited {font-family: "Times New Roman", Times, serif; font-variant: small-caps; color: #CC0000} A.domain-name:hover, A:hover .domain-name {color: #990000} A.domain-name:active, A:active .domain-name {color: #FF6666} .domain-sub {color: #CC0000} .tag-name, A.tag-name:link, A.tag-name:visited {font-family: Arial, Helvetica, sans-serif; font-weight: bold; color: #990000} A.tag-name:hover, A:hover .tag-name {color: #660000} A.tag-name:active, A:active .tag-name {color: #CC3333} .field-name, A.field-name:link, A.field-name:visited {font-family: Arial, Helvetica, sans-serif; color: #663333} A.field-name:hover, A:hover .field-name {color: #333333} A.field-name:active, A:active .field-name {color: #996666} .field-sub {color: #663333} .global-variable, A.global-variable:link, A.global-variable:visited {font-family: "Times New Roman", Times, serif; color: #006600} A.global-variable:hover, A:hover .global-variable {color: #336633} A.global-variable:active, A:active .global-variable {color: #00FF00} .action-name, A.action-name:link, A.action-name:visited {font-family: "Comic Sans MS", "Zapf Chancery", Script, serif; color: #660066} A.action-name:hover, A:hover .action-name {color: #663366} A.action-name:active, A:active .action-name {color: #FF00FF} /* Obsolete styles */ .semantics {margin-left: 9pt; margin-top: 3pt; margin-bottom: 3pt} .semantics-next {margin-left: 27pt; margin-bottom: 3pt} .sub {font-size: 70%} .sub-num {font-size: 70%; font-style: normal} .type-expression {color: #CC0000}