From 85c10d012b05abc37b8690697bff1c737d6351b9 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 27 Jun 2024 10:27:22 -0500
Subject: [PATCH] fix agda colors

---
 src/components/PostList.astro   |   2 +-
 src/pages/posts/[...slug].astro |   5 +-
 src/styles/_colors.scss         | 125 +------------------------
 src/styles/agda.scss            | 159 ++++++++++++++++++++++++++++++++
 src/styles/post.scss            |   1 +
 5 files changed, 165 insertions(+), 127 deletions(-)
 create mode 100644 src/styles/agda.scss

diff --git a/src/components/PostList.astro b/src/components/PostList.astro
index 425cf4a..d642589 100644
--- a/src/components/PostList.astro
+++ b/src/components/PostList.astro
@@ -59,7 +59,7 @@ const sortedPosts = sortBy(allPosts, (post) => -post.data.date);
           <tr class="row">
             <td>
               <div class="title">
-                <a href={`${basePath}/${post.slug}`} class="brand-colorlink">
+                <a href={`${basePath}/${post.slug}/`} class="brand-colorlink">
                   {post.data.title}
                 </a>
               </div>
diff --git a/src/pages/posts/[...slug].astro b/src/pages/posts/[...slug].astro
index 6551b80..7d8d9e0 100644
--- a/src/pages/posts/[...slug].astro
+++ b/src/pages/posts/[...slug].astro
@@ -1,5 +1,6 @@
 ---
 import "../../styles/post.scss";
+import "../../styles/agda.scss";
 import BaseLayout from "../../layouts/BaseLayout.astro";
 import { type CollectionEntry, getCollection } from "astro:content";
 import Timestamp from "../../components/Timestamp.astro";
@@ -66,8 +67,8 @@ const excerpt = remarkPluginFrontmatter.excerpt?.replaceAll("\n", "");
 
       <small class="post-meta">
         Posted on <Timestamp timestamp={post.data.date} />
-         - {remarkPluginFrontmatter.minutesRead}
-         - <a
+        - {remarkPluginFrontmatter.minutesRead}
+        - <a
           href={`https://git.mzhang.io/michael/blog/commits/branch/master/src/content/posts/${post.id}`}
           target="_blank"
           rel="noopener"
diff --git a/src/styles/_colors.scss b/src/styles/_colors.scss
index f8b7ee9..1def76b 100644
--- a/src/styles/_colors.scss
+++ b/src/styles/_colors.scss
@@ -76,127 +76,4 @@
     --astro-code-token-punctuation: #ffab70;
     --astro-code-token-link: black;
   }
-}
-
-pre.Agda {
-  a {
-    color: var(--astro-code-color-text);
-  }
-
-  //   .Keyword {
-  //     color: var(--astro-code-token-keyword);
-  //   }
-
-  //   .Comment {
-  //     color: var(--astro-code-token-comment);
-  //   }
-
-  //   .Symbol {
-  //     color: var(--astro-code-token-punctuation);
-  //   }
-
-  //   .Function {
-  //     color: var(--astro-code-token-function);
-  //   }
-}
-
-/* Aspects. */
-.Agda .Comment {
-  color: #b22222;
-}
-.Agda .Background {
-}
-.Agda .Markup {
-  color: #000000;
-}
-.Agda .Keyword {
-  color: #cd6600;
-}
-.Agda .String {
-  color: #b22222;
-}
-.Agda .Number {
-  color: #a020f0;
-}
-.Agda .Symbol {
-  color: #404040;
-}
-.Agda .PrimitiveType {
-  color: #0000cd;
-}
-.Agda .Pragma {
-  color: black;
-}
-.Agda .Operator {
-}
-
-/* NameKinds. */
-.Agda .Bound {
-  color: black;
-}
-.Agda .Generalizable {
-  color: black;
-}
-.Agda .InductiveConstructor {
-  color: #008b00;
-}
-.Agda .CoinductiveConstructor {
-  color: #8b7500;
-}
-.Agda .Datatype {
-  color: #0000cd;
-}
-.Agda .Field {
-  color: #ee1289;
-}
-.Agda .Function {
-  color: #0000cd;
-}
-.Agda .Module {
-  color: #a020f0;
-}
-.Agda .Postulate {
-  color: #0000cd;
-}
-.Agda .Primitive {
-  color: #0000cd;
-}
-.Agda .Record {
-  color: #0000cd;
-}
-
-/* OtherAspects. */
-.Agda .DottedPattern {
-}
-.Agda .UnsolvedMeta {
-  color: black;
-  background: yellow;
-}
-.Agda .UnsolvedConstraint {
-  color: black;
-  background: yellow;
-}
-.Agda .TerminationProblem {
-  color: black;
-  background: #ffa07a;
-}
-.Agda .IncompletePattern {
-  color: black;
-  background: #f5deb3;
-}
-.Agda .Error {
-  color: red;
-  text-decoration: underline;
-}
-.Agda .TypeChecks {
-  color: black;
-  background: #add8e6;
-}
-
-/* Standard attributes. */
-.Agda a {
-  text-decoration: none;
-}
-// .Agda a[href]:hover {
-//   background-color: #b4eeb4;
-// }
+}
\ No newline at end of file
diff --git a/src/styles/agda.scss b/src/styles/agda.scss
new file mode 100644
index 0000000..6765fb3
--- /dev/null
+++ b/src/styles/agda.scss
@@ -0,0 +1,159 @@
+:root {
+  --default-text: black;
+  --symbol: #404040;
+  --blue: #5175be;
+  --module: purple;
+  --inductive-constructor: #008b00;
+}
+
+@media (prefers-color-scheme: dark) {
+  :root {
+    --default-text: white;
+    --symbol: #b0b0b0;
+    --blue: #9999FF;
+    --module: hsl(276, 66%, 69%);
+    --inductive-constructor: #32bb32;
+  }
+}
+
+/* Aspects. */
+.Agda .Comment {
+  color: #B22222
+}
+
+.Agda .Background {}
+
+.Agda .Markup {
+  color: var(--default-text);
+}
+
+.Agda .Keyword {
+  color: #CD6600
+}
+
+.Agda .String {
+  color: #B22222
+}
+
+.Agda .Number {
+  color: var(--module);
+}
+
+.Agda .Symbol {
+  color: var(--symbol);
+}
+
+.Agda .PrimitiveType {
+  color: var(--blue);
+}
+
+.Agda .Pragma {
+  color: var(--default-text);
+}
+
+.Agda .Operator {}
+
+.Agda .Hole {
+  background: #B4EEB4
+}
+
+/* NameKinds. */
+.Agda .Bound {
+  color: var(--default-text);
+}
+
+.Agda .Generalizable {
+  color: var(--default-text);
+}
+
+.Agda .InductiveConstructor {
+  color: var(--inductive-constructor)
+}
+
+.Agda .CoinductiveConstructor {
+  color: #8B7500
+}
+
+.Agda .Datatype {
+  color: var(--blue);
+}
+
+.Agda .Field {
+  color: #EE1289
+}
+
+.Agda .Function {
+  color: var(--blue);
+}
+
+.Agda .Module {
+  color: var(--module)
+}
+
+.Agda .Postulate {
+  color: var(--blue);
+}
+
+.Agda .Primitive {
+  color: var(--blue);
+}
+
+.Agda .Record {
+  color: var(--blue);
+}
+
+/* OtherAspects. */
+.Agda .DottedPattern {}
+
+.Agda .UnsolvedMeta {
+  color: var(--default-text);
+  background: yellow
+}
+
+.Agda .UnsolvedConstraint {
+  color: var(--default-text);
+  background: yellow
+}
+
+.Agda .TerminationProblem {
+  color: var(--default-text);
+  background: #FFA07A
+}
+
+.Agda .IncompletePattern {
+  color: var(--default-text);
+  background: #F5DEB3
+}
+
+.Agda .Error {
+  color: red;
+  text-decoration: underline
+}
+
+.Agda .TypeChecks {
+  color: var(--default-text);
+  background: #ADD8E6
+}
+
+.Agda .Deadcode {
+  color: var(--default-text);
+  background: #808080
+}
+
+.Agda .ShadowingInTelescope {
+  color: var(--default-text);
+  background: #808080
+}
+
+/* Standard attributes. */
+.Agda a {
+  text-decoration: none
+}
+
+.Agda a[href]:hover {
+  background-color: #B4EEB4
+}
+
+.Agda [href].hover-highlight {
+  background-color: #B4EEB4;
+}
\ No newline at end of file
diff --git a/src/styles/post.scss b/src/styles/post.scss
index 3715ed9..7f75feb 100644
--- a/src/styles/post.scss
+++ b/src/styles/post.scss
@@ -52,6 +52,7 @@
     padding: 12px;
     border-radius: 8px;
     border: 1px solid var(--hr-color);
+    font-family: var(--monofont);
     // background-color: var(--astro-code-color-background);
 
     a {