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