| 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; | |
| } |