548 lines
10 KiB
CSS
Executable File
548 lines
10 KiB
CSS
Executable File
:root {
|
|
--width: 740px;
|
|
--lighter: #fff;
|
|
--light: #fff;
|
|
--mild: #d8dee9;
|
|
/* --dark: #4c566a; */
|
|
--darker: #434c5e;
|
|
--black: #3b4252;
|
|
--blacker: #2e3440;
|
|
--yellow: #f8c325;
|
|
--red: #ee4242;
|
|
--pink: #de59a8;
|
|
|
|
--background: #eee;
|
|
--text-strong: #434c5e;
|
|
--text: #4c566a;
|
|
--dark: #d8dee9;
|
|
--darker: #d8dee9;
|
|
}
|
|
|
|
@media (prefers-color-scheme: dark) {
|
|
:root {
|
|
--background: #3b4252;
|
|
--dark: #3b4252;
|
|
--darker: #2e3440;
|
|
--text-strong: #fff;
|
|
--text: #d8dee9;
|
|
--text-faded: #9ea6b5;
|
|
}
|
|
}
|
|
|
|
|
|
body {
|
|
font: 16px "Inter UI", Inter, sans-serif;
|
|
line-height: 1.54;
|
|
margin: 0;
|
|
min-height: 100vh;
|
|
color: var(--text);
|
|
background: var(--background);
|
|
display: flex;
|
|
flex-direction: column;
|
|
hyphens: auto;
|
|
font-weight: 400;
|
|
counter-reset: section;
|
|
}
|
|
|
|
@media (prefers-color-scheme: dark) {
|
|
body {font-weight: 300}
|
|
}
|
|
|
|
main span.draft {
|
|
display: inline-block;
|
|
text-transform: uppercase;
|
|
background: var(--mild);
|
|
font-size: .8rem;
|
|
padding: .2em .5em;
|
|
border-radius: 3px;
|
|
font-weight: 300;
|
|
vertical-align: middle;
|
|
}
|
|
|
|
h1, h2, h3 { color: var(--darkr) }
|
|
|
|
main > section { counter-reset: subsection }
|
|
main :first-child { margin-top: 0 }
|
|
|
|
main ::selection {
|
|
background: var(--yellow);
|
|
color: var(--black);
|
|
font-weight: 400;
|
|
}
|
|
|
|
section.footnotes {
|
|
margin-top: 3em;
|
|
}
|
|
a.footnote-ref sup::before { content: '[' }
|
|
a.footnote-ref sup::after { content: ']' }
|
|
|
|
.post h2::before {
|
|
counter-increment: section;
|
|
padding: 0 .5em 0 0;
|
|
content: counter(section);
|
|
opacity: .3;
|
|
}
|
|
|
|
.post section h3::before {
|
|
counter-increment: subsection;
|
|
padding: 0 .5em 0 0;
|
|
content: counter(section) "." counter(subsection);
|
|
opacity: .3;
|
|
}
|
|
|
|
a {
|
|
color: inherit;
|
|
font-weight: 400;
|
|
text-decoration: none;
|
|
box-shadow: 0 1px 0 #999;
|
|
}
|
|
|
|
/* a:hover {text-decoration: underline} */
|
|
|
|
hr {
|
|
border: none;
|
|
height: 2px;
|
|
background: var(--darker);
|
|
margin: 2.5em 0;
|
|
}
|
|
|
|
#pidx {
|
|
list-style: none;
|
|
padding: 0;
|
|
margin: 2em 0 0;
|
|
}
|
|
#pidx li {line-height: 1.6em}
|
|
#pidx li > span {
|
|
font-family: monospace;
|
|
font-size: 14px;
|
|
margin-right: 1em;
|
|
opacity: 0.7;
|
|
}
|
|
|
|
details summary {
|
|
cursor: pointer;
|
|
padding: .5em 1em;
|
|
border-radius: 3px;
|
|
}
|
|
|
|
strong {
|
|
color: var(--text-strong);
|
|
font-weight: 500;
|
|
}
|
|
|
|
#hd {
|
|
margin: 1em 0 0;
|
|
}
|
|
|
|
#hd a {box-shadow: none}
|
|
|
|
#hd > section {
|
|
max-width: var(--width);
|
|
margin: 0 auto;
|
|
padding: 0 1em;
|
|
box-sizing: border-box;
|
|
display: flex;
|
|
width: 100%;
|
|
}
|
|
|
|
#hd svg path {
|
|
stroke: var(--text) !important
|
|
}
|
|
|
|
#hd section > a {
|
|
margin: 0 1em 0 0;
|
|
display: flex;
|
|
align-items: center;
|
|
}
|
|
|
|
#hd nav a {
|
|
margin: 0 0 0 1.2rem;
|
|
text-decoration: none;
|
|
text-transform: uppercase;
|
|
font-weight: 500;
|
|
}
|
|
|
|
#hd nav a:hover {border-bottom:2px solid var(--yellow)}
|
|
|
|
main, #ft, .breadcrumb {
|
|
padding: 2em 1em;
|
|
max-width: var(--width);
|
|
box-sizing: border-box;
|
|
width: 100%;
|
|
margin: 0em auto;
|
|
}
|
|
|
|
#ft {
|
|
padding-bottom: 1.5em;
|
|
}
|
|
|
|
main {
|
|
padding: 0 1em;
|
|
margin: 2em auto;
|
|
}
|
|
|
|
p > span.display {
|
|
display: block;
|
|
overflow-x: auto;
|
|
overflow-y: clip;
|
|
margin: 2em 0;
|
|
}
|
|
|
|
p > span.display .katex { display:block } /* katex is shit */
|
|
|
|
p > span.display math {
|
|
font-size: 1.2rem;
|
|
}
|
|
|
|
|
|
main {flex-grow: 1 }
|
|
|
|
h1, h2, h3, h4 { font-weight: 500 }
|
|
|
|
main header h1 {margin: 0}
|
|
main header p {margin: 0}
|
|
main header {margin: 0 0 2em}
|
|
|
|
main ul li, main ol li { padding: 0 0 0 0 }
|
|
main ul, main ol { padding: 0 0 0 1.5em }
|
|
|
|
main ul.projects a { text-decoration: none; box-shadow: none }
|
|
|
|
main ul.projects {
|
|
padding: 0;
|
|
margin: 2.5em 0 0;
|
|
list-style: none;
|
|
display: grid;
|
|
grid-template-columns: repeat(auto-fill, minmax(300px, 1fr));
|
|
grid-gap: 1.5em;
|
|
}
|
|
|
|
main ul.projects li {
|
|
border-radius: 5px;
|
|
}
|
|
|
|
main ul.projects > li > a {
|
|
display: flex;
|
|
color: inherit;
|
|
transition: .2s background
|
|
}
|
|
|
|
main ul.projects li a p {
|
|
font-weight: 300;
|
|
opacity: 0.7;
|
|
font-size: .9em;
|
|
margin: 0;
|
|
}
|
|
|
|
main ul.projects > li svg {
|
|
width: 40px;
|
|
margin: .5em 1em 0 0;
|
|
}
|
|
|
|
main ul.projects > li svg rect,
|
|
main ul.projects > li svg path,
|
|
main ul.projects > li svg use,
|
|
header.project div svg rect,
|
|
header.project div svg path,
|
|
header.project div svg use {
|
|
fill: none;
|
|
stroke: var(--text);
|
|
stroke-linejoin: bevel;
|
|
stroke-linecap: round;
|
|
}
|
|
|
|
main ul.projects > li h2 { margin: 0; font-size: 1em }
|
|
|
|
|
|
header.project { display: flex }
|
|
header.project svg {
|
|
width: 40px;
|
|
margin: 1em 2em 0 0;
|
|
}
|
|
header.project p {font-style: italic}
|
|
header.project ul {padding: 0}
|
|
header.project ul li {
|
|
font-size: .9em;
|
|
display: inline-block;
|
|
padding: .3em .5em;
|
|
font-family: monospace;
|
|
border-radius: 3px;
|
|
margin: 0 1em 0 0;
|
|
}
|
|
|
|
main blockquote {
|
|
border-left: 2px solid var(--darker);
|
|
margin: 1.5em 0;
|
|
padding: 0 1em;
|
|
opacity: 0.8;
|
|
line-height: 1.5;
|
|
font-style: italic;
|
|
}
|
|
|
|
main h2 { font-size: 1.6em; margin: 1em 0 .5em }
|
|
main h1 + h2 {margin-top: 0}
|
|
main h3 { font-size: 1.3em; margin: 1em 0 .5em }
|
|
|
|
#citations {margin: 2em 0 0}
|
|
dl {display:grid; gap: 1em; grid-template-columns: auto 1fr}
|
|
dt {text-align: right; font-weight: 500;}
|
|
.citation-label::before {content:'['}
|
|
.citation-label::after {content:']:'}
|
|
dd {margin:0}
|
|
dd p {margin:0}
|
|
|
|
code, pre.Agda {font: 1em monospace}
|
|
pre.Agda a {font-weight: inherit; text-decoration: none}
|
|
pre.Agda a[href]:hover { box-shadow: 0 2px 0 var(--yellow) }
|
|
|
|
code {
|
|
display: inline-block;
|
|
padding: 0 .3em;
|
|
background: var(--dark);
|
|
}
|
|
|
|
pre > code {display: block}
|
|
|
|
pre, div.sourceCode {
|
|
margin:1.5em 0;
|
|
padding: .8em 0;
|
|
line-height: 1;
|
|
overflow: auto;
|
|
}
|
|
|
|
pre, div.sourceCode {
|
|
background: var(--dark);
|
|
}
|
|
|
|
div.sourceCode > pre {
|
|
margin: 0;
|
|
padding: 0;
|
|
}
|
|
|
|
pre.Agda {
|
|
margin: 1.5em 0;
|
|
padding: .8em 1em;
|
|
overflow: auto;
|
|
}
|
|
|
|
pre > code {
|
|
display: inline-block;
|
|
margin: 0 1em;
|
|
}
|
|
|
|
figure {
|
|
margin: 2em 0;
|
|
text-align: center;
|
|
counter-increment: figure;
|
|
}
|
|
figure figcaption {
|
|
margin-top: 1em;
|
|
}
|
|
|
|
figure figcaption::before {
|
|
content: "Fig " counter(figure) ".";
|
|
padding-right: .5em;
|
|
font-style: italic;
|
|
font-weight: 400;
|
|
}
|
|
|
|
figure table {
|
|
margin: 0 auto;
|
|
border-collapse: collapse;
|
|
}
|
|
|
|
figure table th { font-weight: 500 }
|
|
figure table th, figure table td {
|
|
border: 2px solid var(--darker);
|
|
padding: .3em .5em;
|
|
}
|
|
|
|
ol.pages {
|
|
padding: .5em 1em .5em 3em;
|
|
margin: 2em 0 2.5em;
|
|
}
|
|
ol.pages li::marker {
|
|
font-weight: 600;
|
|
color: var(--dark);
|
|
}
|
|
|
|
ol.pages li a {
|
|
display: block;
|
|
line-height: 2em;
|
|
padding: 0 1em;
|
|
}
|
|
|
|
section.visual {
|
|
display: grid;
|
|
grid-gap: 1em;
|
|
align-items: center;
|
|
grid-template-columns: repeat(auto-fill, minmax(300px, 1fr));
|
|
}
|
|
|
|
section.visual:not(.tiny) {
|
|
grid-template-rows: masonry;
|
|
}
|
|
|
|
section.visual.tiny {
|
|
align-items: stretch;
|
|
grid-template-columns: repeat(auto-fill, minmax(160px, 1fr));
|
|
}
|
|
|
|
section.visual figure { margin: 0 }
|
|
section.visual.tiny figure { margin: 0; overflow: hidden; }
|
|
figure img {
|
|
max-width: 100%;
|
|
height: auto;
|
|
/* aspect-ratio: attr(width) / attr(height); */
|
|
vertical-align: top;
|
|
}
|
|
section.visual.tiny img {object-fit: cover}
|
|
|
|
p.right {text-align: right}
|
|
|
|
section.visual.tiny figure img { height: 100% }
|
|
|
|
.admonition {
|
|
border-left: 3px solid var(--yellow);
|
|
box-sizing: border-box;
|
|
padding: 1px 1em;
|
|
background: #f8c32520;
|
|
border-radius: 3px;
|
|
font-weight: 300;
|
|
font-size: .9rem;
|
|
color: #67510f
|
|
}
|
|
|
|
.admonition p {
|
|
margin: .5em 0;
|
|
}
|
|
|
|
.al {color: #f00; font-weight: bold; }
|
|
.an {color: #60a0b0; font-weight: bold; font-style: italic; }
|
|
.at {color:#7d9029}
|
|
.bn {color:#40a070}
|
|
.cf {color:#007020; font-weight: bold; }
|
|
.ch {color:#4070a0}
|
|
.cn, .Agda .InductiveConstructor {color:#880000}
|
|
.co, .Agda .Comment {color:#60a0b0; font-style: italic; }
|
|
.cv {color:#60a0b0; font-weight: bold; font-style: italic; }
|
|
.do {color:#ba2121; font-style: italic; }
|
|
.dt, .Agda .PrimitiveType
|
|
, .Agda .Datatype {color:#902000}
|
|
.dv {color:#40a070}
|
|
.er {color:#f00; font-weight: bold; }
|
|
.fl {color:#40a070; }
|
|
.fu, .Agda .Function {color:#06287e; }
|
|
.in {color:#60a0b0; font-weight: bold; font-style: italic; }
|
|
.kw, .Agda .Keyword {color:#007020; }
|
|
.op {color:#666}
|
|
.ot, .Agda .Symbol {color:#007020}
|
|
.pp {color:#bc7a00}
|
|
.sc {color:#4070a0}
|
|
.ss {color:#bb6688}
|
|
.st {color:#4070a0}
|
|
.va {color:#19177c}
|
|
.vs {color:#4070a0}
|
|
.wa {color:#60a0b0; font-weight: bold; font-style: italic; }
|
|
|
|
@media (prefers-color-scheme: dark) {
|
|
.al {color: #DC322F; font-weight: bold; }
|
|
.an {color: #60a0b0; font-weight: bold; font-style: italic; }
|
|
.at {color:#7d9029}
|
|
.bn {color:#40a070}
|
|
.cf {color:#007020; font-weight: bold; }
|
|
.ch {color:#4070a0}
|
|
.cn, .Agda .InductiveConstructor, .Field {color:#2AA198}
|
|
.co, .Agda .Comment {color:#60a0b0; font-style: italic; }
|
|
.cv {color:#60a0b0; font-weight: bold; font-style: italic; }
|
|
.do {color:#ba2121; font-style: italic; }
|
|
.dt, .Agda .PrimitiveType
|
|
, .Agda .Datatype {color:#B58900}
|
|
.dv {color:#40a070}
|
|
.er {color:#f00; font-weight: bold; }
|
|
.fl {color:#40a070; }
|
|
.fu, .Agda .Function {color:#268BD2; }
|
|
.in {color:#60a0b0; font-weight: bold; font-style: italic; }
|
|
.kw, .Agda .Keyword {color: #859900; }
|
|
.op {color:#666}
|
|
.ot, .Agda .Symbol {color:#93A1A1}
|
|
.pp {color:#bc7a00}
|
|
.sc {color:#4070a0}
|
|
.ss {color:#bb6688}
|
|
.st {color:#4070a0}
|
|
.va {color:#19177c}
|
|
.vs {color:#4070a0}
|
|
.wa {color:#60a0b0; font-weight: bold; font-style: italic; }
|
|
|
|
div.sourceCode, pre.Agda, code, pre {
|
|
background: #2f3542;
|
|
}
|
|
}
|
|
|
|
table.books {
|
|
border-collapse: collapse;
|
|
margin: 0 auto;
|
|
}
|
|
table.books tr td {
|
|
padding: .1em 1em
|
|
}
|
|
table.books tr td:first-child {
|
|
font-style: italic;
|
|
text-align: right;
|
|
color: var(--text-faded);
|
|
font-weight: 500;
|
|
}
|
|
|
|
table.books tr td:nth-child(3),
|
|
table.books tr td:last-child {text-align: center;color: var(--yellow)}
|
|
|
|
.breadcrumb {
|
|
padding-bottom: 0;
|
|
padding-top: 0;
|
|
margin-top: 2em;
|
|
}
|
|
|
|
.breadcrumb .sep {
|
|
color: #999;
|
|
padding: 0 .5em;
|
|
cursor: default;
|
|
}
|
|
|
|
main { counter-reset: figure; }
|
|
main > header h1 {line-height: 1.3 }
|
|
main > header time {
|
|
opacity: 0.6;
|
|
}
|
|
|
|
canvas { width: 100% }
|
|
canvas.r1 { aspect-ratio: 1 }
|
|
canvas.r2 { aspect-ratio: 2 }
|
|
canvas.hw { width: 50% }
|
|
|
|
input[type=range] {
|
|
width: calc(100% - 2em);
|
|
margin: 1em 1em;
|
|
box-sizing: border-box;
|
|
display: block;
|
|
}
|
|
|
|
.grabber { cursor: grab }
|
|
|
|
/* MathML styling */
|
|
mover.seq > mrow:nth-child(2) { /* display: block */ }
|
|
mover.seq > mrow:nth-child(1) {
|
|
border-top: .05em solid;
|
|
}
|
|
mover.seq > mrow:nth-child(2) {
|
|
padding-bottom: .1em;
|
|
border-bottom: .05em solid;
|
|
/* display: flex;
|
|
flex-direction: row;
|
|
gap: 1em;
|
|
justify-content: space-between; */
|
|
}
|
|
mover.seq > mrow { math-depth: 0 }
|
|
mover.seq > mrow:nth-child(2) > * {
|
|
align-self: end;
|
|
}
|