style.css

@import "https://monade.li/main.css";

:root {
  --accent2: #6ecfff;

  --comment: hsl(0, 0%, 65%);
  --defined: var(--foreground);
  --bound: var(--accent);
  --literal: var(--accent2);
  --keyword: var(--foreground);
  --symbol: var(--foreground);
  --module: var(--bound);
  --constructor: var(--literal);
}

body {
  max-width: 60em;
  text-align: justify;
}

blockquote {
  text-align: initial;
}

pre {
  /* Otherwise Firefox takes ages trying to justify <pre> blocks... */
  text-align: initial;

  overflow-x: auto;
}

.katex {
  /* Defaults to 1.21em, which is a bit much.
     https://katex.org/docs/font.html#font-size-and-lengths */
  font-size: 1.08em;
}

.katex-html {
  /* Prevents browsers from inserting a line break just before punctuation following
     inline maths https://github.com/KaTeX/KaTeX/issues/1233 */
  white-space: nowrap;
}

.diagram-container {
  text-align: center;
  overflow-x: auto;
}

.anchor {
  margin-left: 10px;
  font-size: 80%;
  opacity: 0;
}

.anchor::before {
  content: '🔗';
}

h1:hover > .anchor, h2:hover > .anchor, h3:hover > .anchor, h4:hover > .anchor, h5:hover > .anchor, h6:hover > .anchor {
  opacity: 1;
}

/* Aspects. */
.Agda .Comment       { color: var(--comment) }
.Agda .Background    { }
.Agda .Markup        { }
.Agda .Keyword       { color: var(--keyword); font-weight: bold; }
.Agda .String        { color: var(--literal) }
.Agda .Number        { color: var(--literal) }
.Agda .Symbol        { color: var(--symbol) }
.Agda .PrimitiveType { color: var(--defined) }
.Agda .Pragma        { color: var(--keyword)   }
.Agda .Operator      {}
.Agda .Hole          { background: #e4cbef; color: #14111c }
.Agda .Macro         { color: var(--defined) }

/* NameKinds. */
.Agda .Bound                  { color: var(--bound)   }
.Agda .Generalizable          { color: var(--bound)   }
.Agda .InductiveConstructor   { color: var(--constructor) }
.Agda .CoinductiveConstructor { color: var(--constructor) }
.Agda .Datatype               { color: var(--defined) }
.Agda .Field                  { color: var(--constructor) }
.Agda .Function               { color: var(--defined) }
.Agda .Module                 { color: var(--module) }
.Agda .Postulate              { color: var(--defined) }
.Agda .Primitive              { color: var(--defined) }
.Agda .Record                 { color: var(--defined) }

/* OtherAspects. */
.Agda .DottedPattern        {}
.Agda .UnsolvedMeta         { color: var(--foreground); background: yellow         }
.Agda .UnsolvedConstraint   { color: var(--foreground); background: yellow         }
.Agda .TerminationProblem   { color: var(--foreground); background: #FFA07A        }
.Agda .IncompletePattern    { color: var(--foreground); background: #F5DEB3        }
.Agda .Error                { color: red;   text-decoration: underline }
.Agda .TypeChecks           { color: var(--foreground); background: #ADD8E6        }
.Agda .Deadcode             { color: var(--foreground); background: #808080        }
.Agda .ShadowingInTelescope { color: var(--foreground); background: #808080        }