| table.calltree { |
| width : 100%; |
| } |
| |
| td { |
| padding-top: 0.1em; |
| padding-bottom: 0.1em; |
| } |
| |
| .numeric { |
| width : 12ex; |
| } |
| |
| .numeric-hidden { |
| display : none; |
| } |
| |
| body { |
| font-family: 'Roboto', sans-serif; |
| } |
| |
| #source-status { |
| display: inline-block; |
| } |
| |
| .tree-row-arrow { |
| margin-right: 0.2em; |
| text-align: right; |
| } |
| |
| .code-type-chip { |
| border-radius : 1em; |
| padding : 0.2em; |
| background-color : #4040c0; |
| color: #ffffff; |
| font-size : small; |
| box-shadow: 0 2px 5px 0 rgba(0, 0, 0, 0.16), 0 2px 10px 0 rgba(0, 0, 0, 0.12); |
| } |
| |
| .tree-row-name { |
| margin-left: 0.2em; |
| margin-right: 0.2em; |
| } |
| |
| .codeid-link { |
| text-decoration: underline; |
| cursor: pointer; |
| } |
| |
| .view-source-link { |
| text-decoration: underline; |
| cursor: pointer; |
| font-size: 10pt; |
| margin-left: 0.6em; |
| color: #555555; |
| } |
| |
| #source-viewer { |
| border: 1px solid black; |
| padding: 0.2em; |
| font-family: 'Roboto Mono', monospace; |
| white-space: pre; |
| margin-top: 1em; |
| margin-bottom: 1em; |
| } |
| |
| #source-viewer td.line-none { |
| background-color: white; |
| } |
| |
| #source-viewer td.line-cold { |
| background-color: #e1f5fe; |
| } |
| |
| #source-viewer td.line-mediumcold { |
| background-color: #b2ebf2; |
| } |
| |
| #source-viewer td.line-mediumhot { |
| background-color: #c5e1a5; |
| } |
| |
| #source-viewer td.line-hot { |
| background-color: #dce775; |
| } |
| |
| #source-viewer td.line-superhot { |
| background-color: #ffee58; |
| } |
| |
| #source-viewer .source-line-number { |
| padding-left: 0.2em; |
| padding-right: 0.2em; |
| color: #003c8f; |
| background-color: #eceff1; |
| } |
| |
| div.mode-button { |
| padding: 1em 3em; |
| display: inline-block; |
| background-color: #6070ff; |
| color : #ffffff; |
| margin: 0 0.2em 2em 0; |
| box-shadow: 3px 3px 2px #d0d0ff; |
| } |
| |
| div.mode-button:hover { |
| background-color: #4858ff; |
| } |
| |
| div.active-mode-button { |
| background-color: #0000ff; |
| box-shadow: 3px 3px 2px #a0a0ff; |
| } |
| |
| div.active-mode-button:hover { |
| background-color: #0000ff; |
| } |