agda fix

astro.config.ts

@@ -11,7 +11,7 @@ import remarkAdmonitions from "./plugin/remark-admonitions";
 import remarkMath from "remark-math";
 import rehypeKatex from "rehype-katex";
 
-import addProofMacros from "./utils/mzproofs";
+// import addProofMacros from "./utils/mzproofs";
 import remarkAgda from "./plugin/remark-agda";
 
 // https://astro.build/config
@@ -34,6 +34,14 @@ export default defineConfig({
       emoji,
       [remarkDescription, { name: "excerpt" }],
     ],
-    rehypePlugins: [[rehypeKatex, { macros: addProofMacros({}) }], rehypeAccessibleEmojis],
+    rehypePlugins: [
+      [
+        rehypeKatex,
+        {
+          // macros: addProofMacros({})
+        },
+      ],
+      rehypeAccessibleEmojis,
+    ],
   },
 });

package-lock.json

@@ -31,6 +31,8 @@
       },
       "devDependencies": {
         "@types/lodash-es": "^4.17.9",
+        "hast-util-from-html": "^2.0.1",
+        "hast-util-to-html": "^9.0.0",
         "mdast": "^3.0.0",
         "mdast-util-from-markdown": "^2.0.0",
         "prettier": "^3.0.3",
@@ -3459,6 +3461,28 @@
         "astro": "^3.2.3"
       }
     },
+    "node_modules/@astrojs/mdx/node_modules/hast-util-to-html": {
+      "version": "8.0.4",
+      "resolved": "https://registry.npmjs.org/hast-util-to-html/-/hast-util-to-html-8.0.4.tgz",
+      "integrity": "sha512-4tpQTUOr9BMjtYyNlt0P50mH7xj0Ks2xpo8M943Vykljf99HW6EzulIoJP1N3eKOSScEHzyzi9dm7/cn0RfGwA==",
+      "dependencies": {
+        "@types/hast": "^2.0.0",
+        "@types/unist": "^2.0.0",
+        "ccount": "^2.0.0",
+        "comma-separated-tokens": "^2.0.0",
+        "hast-util-raw": "^7.0.0",
+        "hast-util-whitespace": "^2.0.0",
+        "html-void-elements": "^2.0.0",
+        "property-information": "^6.0.0",
+        "space-separated-tokens": "^2.0.0",
+        "stringify-entities": "^4.0.0",
+        "zwitch": "^2.0.4"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
     "node_modules/@astrojs/mdx/node_modules/unist-util-visit": {
       "version": "4.1.2",
       "license": "MIT",
@@ -4261,13 +4285,6 @@
         "unist-util-visit": "^4.1.1"
       }
     },
-    "node_modules/astro-remark-description/node_modules/@types/hast": {
-      "version": "3.0.1",
-      "license": "MIT",
-      "dependencies": {
-        "@types/unist": "*"
-      }
-    },
     "node_modules/astro-remark-description/node_modules/@types/mdast": {
       "version": "3.0.13",
       "license": "MIT",
@@ -4275,167 +4292,6 @@
         "@types/unist": "^2"
       }
     },
-    "node_modules/astro-remark-description/node_modules/hast-util-from-parse5": {
-      "version": "8.0.1",
-      "license": "MIT",
-      "dependencies": {
-        "@types/hast": "^3.0.0",
-        "@types/unist": "^3.0.0",
-        "devlop": "^1.0.0",
-        "hastscript": "^8.0.0",
-        "property-information": "^6.0.0",
-        "vfile": "^6.0.0",
-        "vfile-location": "^5.0.0",
-        "web-namespaces": "^2.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/hast-util-from-parse5/node_modules/@types/unist": {
-      "version": "3.0.0",
-      "license": "MIT"
-    },
-    "node_modules/astro-remark-description/node_modules/hast-util-parse-selector": {
-      "version": "4.0.0",
-      "license": "MIT",
-      "dependencies": {
-        "@types/hast": "^3.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/hast-util-raw": {
-      "version": "9.0.1",
-      "license": "MIT",
-      "dependencies": {
-        "@types/hast": "^3.0.0",
-        "@types/unist": "^3.0.0",
-        "@ungap/structured-clone": "^1.0.0",
-        "hast-util-from-parse5": "^8.0.0",
-        "hast-util-to-parse5": "^8.0.0",
-        "html-void-elements": "^3.0.0",
-        "mdast-util-to-hast": "^13.0.0",
-        "parse5": "^7.0.0",
-        "unist-util-position": "^5.0.0",
-        "unist-util-visit": "^5.0.0",
-        "vfile": "^6.0.0",
-        "web-namespaces": "^2.0.0",
-        "zwitch": "^2.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/hast-util-raw/node_modules/@types/unist": {
-      "version": "3.0.0",
-      "license": "MIT"
-    },
-    "node_modules/astro-remark-description/node_modules/hast-util-raw/node_modules/unist-util-is": {
-      "version": "6.0.0",
-      "license": "MIT",
-      "dependencies": {
-        "@types/unist": "^3.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/hast-util-raw/node_modules/unist-util-visit": {
-      "version": "5.0.0",
-      "license": "MIT",
-      "dependencies": {
-        "@types/unist": "^3.0.0",
-        "unist-util-is": "^6.0.0",
-        "unist-util-visit-parents": "^6.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/hast-util-to-html": {
-      "version": "9.0.0",
-      "license": "MIT",
-      "dependencies": {
-        "@types/hast": "^3.0.0",
-        "@types/unist": "^3.0.0",
-        "ccount": "^2.0.0",
-        "comma-separated-tokens": "^2.0.0",
-        "hast-util-raw": "^9.0.0",
-        "hast-util-whitespace": "^3.0.0",
-        "html-void-elements": "^3.0.0",
-        "mdast-util-to-hast": "^13.0.0",
-        "property-information": "^6.0.0",
-        "space-separated-tokens": "^2.0.0",
-        "stringify-entities": "^4.0.0",
-        "zwitch": "^2.0.4"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/hast-util-to-html/node_modules/@types/unist": {
-      "version": "3.0.0",
-      "license": "MIT"
-    },
-    "node_modules/astro-remark-description/node_modules/hast-util-to-parse5": {
-      "version": "8.0.0",
-      "license": "MIT",
-      "dependencies": {
-        "@types/hast": "^3.0.0",
-        "comma-separated-tokens": "^2.0.0",
-        "devlop": "^1.0.0",
-        "property-information": "^6.0.0",
-        "space-separated-tokens": "^2.0.0",
-        "web-namespaces": "^2.0.0",
-        "zwitch": "^2.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/hast-util-whitespace": {
-      "version": "3.0.0",
-      "license": "MIT",
-      "dependencies": {
-        "@types/hast": "^3.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/hastscript": {
-      "version": "8.0.0",
-      "license": "MIT",
-      "dependencies": {
-        "@types/hast": "^3.0.0",
-        "comma-separated-tokens": "^2.0.0",
-        "hast-util-parse-selector": "^4.0.0",
-        "property-information": "^6.0.0",
-        "space-separated-tokens": "^2.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/html-void-elements": {
-      "version": "3.0.0",
-      "license": "MIT",
-      "funding": {
-        "type": "github",
-        "url": "https://github.com/sponsors/wooorm"
-      }
-    },
     "node_modules/astro-remark-description/node_modules/mdast-util-to-string": {
       "version": "3.2.0",
       "license": "MIT",
@@ -4447,46 +4303,6 @@
         "url": "https://opencollective.com/unified"
       }
     },
-    "node_modules/astro-remark-description/node_modules/parse5": {
-      "version": "7.1.2",
-      "license": "MIT",
-      "dependencies": {
-        "entities": "^4.4.0"
-      },
-      "funding": {
-        "url": "https://github.com/inikulin/parse5?sponsor=1"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/unist-util-position": {
-      "version": "5.0.0",
-      "license": "MIT",
-      "dependencies": {
-        "@types/unist": "^3.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/unist-util-position/node_modules/@types/unist": {
-      "version": "3.0.0",
-      "license": "MIT"
-    },
-    "node_modules/astro-remark-description/node_modules/unist-util-stringify-position": {
-      "version": "4.0.0",
-      "license": "MIT",
-      "dependencies": {
-        "@types/unist": "^3.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/unist-util-stringify-position/node_modules/@types/unist": {
-      "version": "3.0.0",
-      "license": "MIT"
-    },
     "node_modules/astro-remark-description/node_modules/unist-util-visit": {
       "version": "4.1.2",
       "license": "MIT",
@@ -4512,55 +4328,6 @@
         "url": "https://opencollective.com/unified"
       }
     },
-    "node_modules/astro-remark-description/node_modules/vfile": {
-      "version": "6.0.1",
-      "license": "MIT",
-      "dependencies": {
-        "@types/unist": "^3.0.0",
-        "unist-util-stringify-position": "^4.0.0",
-        "vfile-message": "^4.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/vfile-location": {
-      "version": "5.0.2",
-      "license": "MIT",
-      "dependencies": {
-        "@types/unist": "^3.0.0",
-        "vfile": "^6.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/vfile-location/node_modules/@types/unist": {
-      "version": "3.0.0",
-      "license": "MIT"
-    },
-    "node_modules/astro-remark-description/node_modules/vfile-message": {
-      "version": "4.0.2",
-      "license": "MIT",
-      "dependencies": {
-        "@types/unist": "^3.0.0",
-        "unist-util-stringify-position": "^4.0.0"
-      },
-      "funding": {
-        "type": "opencollective",
-        "url": "https://opencollective.com/unified"
-      }
-    },
-    "node_modules/astro-remark-description/node_modules/vfile-message/node_modules/@types/unist": {
-      "version": "3.0.0",
-      "license": "MIT"
-    },
-    "node_modules/astro-remark-description/node_modules/vfile/node_modules/@types/unist": {
-      "version": "3.0.0",
-      "license": "MIT"
-    },
     "node_modules/bail": {
       "version": "2.0.2",
       "license": "MIT",
@@ -5699,14 +5466,17 @@
       }
     },
     "node_modules/hast-util-from-html": {
-      "version": "1.0.2",
+      "version": "2.0.1",
-      "license": "MIT",
+      "resolved": "https://registry.npmjs.org/hast-util-from-html/-/hast-util-from-html-2.0.1.tgz",
+      "integrity": "sha512-RXQBLMl9kjKVNkJTIO6bZyb2n+cUH8LFaSSzo82jiLT6Tfc+Pt7VQCS+/h3YwG4jaNE2TA2sdJisGWR+aJrp0g==",
+      "dev": true,
       "dependencies": {
-        "@types/hast": "^2.0.0",
+        "@types/hast": "^3.0.0",
-        "hast-util-from-parse5": "^7.0.0",
+        "devlop": "^1.1.0",
+        "hast-util-from-parse5": "^8.0.0",
         "parse5": "^7.0.0",
-        "vfile": "^5.0.0",
+        "vfile": "^6.0.0",
-        "vfile-message": "^3.0.0"
+        "vfile-message": "^4.0.0"
       },
       "funding": {
         "type": "opencollective",
@@ -5727,8 +5497,101 @@
         "url": "https://opencollective.com/unified"
       }
     },
+    "node_modules/hast-util-from-html-isomorphic/node_modules/hast-util-from-html": {
+      "version": "1.0.2",
+      "resolved": "https://registry.npmjs.org/hast-util-from-html/-/hast-util-from-html-1.0.2.tgz",
+      "integrity": "sha512-LhrTA2gfCbLOGJq2u/asp4kwuG0y6NhWTXiPKP+n0qNukKy7hc10whqqCFfyvIA1Q5U5d0sp9HhNim9gglEH4A==",
+      "dependencies": {
+        "@types/hast": "^2.0.0",
+        "hast-util-from-parse5": "^7.0.0",
+        "parse5": "^7.0.0",
+        "vfile": "^5.0.0",
+        "vfile-message": "^3.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-from-html-isomorphic/node_modules/parse5": {
+      "version": "7.1.2",
+      "resolved": "https://registry.npmjs.org/parse5/-/parse5-7.1.2.tgz",
+      "integrity": "sha512-Czj1WaSVpaoj0wbhMzLmWD69anp2WH7FXMB9n1Sy8/ZFF9jolSQVMu1Ij5WIyGmcBmhk7EOndpO4mIpihVqAXw==",
+      "dependencies": {
+        "entities": "^4.4.0"
+      },
+      "funding": {
+        "url": "https://github.com/inikulin/parse5?sponsor=1"
+      }
+    },
+    "node_modules/hast-util-from-html/node_modules/@types/hast": {
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/@types/hast/-/hast-3.0.1.tgz",
+      "integrity": "sha512-hs/iBJx2aydugBQx5ETV3ZgeSS0oIreQrFJ4bjBl0XvM4wAmDjFEALY7p0rTSLt2eL+ibjRAAs9dTPiCLtmbqQ==",
+      "dev": true,
+      "dependencies": {
+        "@types/unist": "*"
+      }
+    },
+    "node_modules/hast-util-from-html/node_modules/@types/unist": {
+      "version": "3.0.0",
+      "resolved": "https://registry.npmjs.org/@types/unist/-/unist-3.0.0.tgz",
+      "integrity": "sha512-MFETx3tbTjE7Uk6vvnWINA/1iJ7LuMdO4fcq8UfF0pRbj01aGLduVvQcRyswuACJdpnHgg8E3rQLhaRdNEJS0w==",
+      "dev": true
+    },
+    "node_modules/hast-util-from-html/node_modules/hast-util-from-parse5": {
+      "version": "8.0.1",
+      "resolved": "https://registry.npmjs.org/hast-util-from-parse5/-/hast-util-from-parse5-8.0.1.tgz",
+      "integrity": "sha512-Er/Iixbc7IEa7r/XLtuG52zoqn/b3Xng/w6aZQ0xGVxzhw5xUFxcRqdPzP6yFi/4HBYRaifaI5fQ1RH8n0ZeOQ==",
+      "dev": true,
+      "dependencies": {
+        "@types/hast": "^3.0.0",
+        "@types/unist": "^3.0.0",
+        "devlop": "^1.0.0",
+        "hastscript": "^8.0.0",
+        "property-information": "^6.0.0",
+        "vfile": "^6.0.0",
+        "vfile-location": "^5.0.0",
+        "web-namespaces": "^2.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-from-html/node_modules/hast-util-parse-selector": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/hast-util-parse-selector/-/hast-util-parse-selector-4.0.0.tgz",
+      "integrity": "sha512-wkQCkSYoOGCRKERFWcxMVMOcYE2K1AaNLU8DXS9arxnLOUEWbOXKXiJUNzEpqZ3JOKpnha3jkFrumEjVliDe7A==",
+      "dev": true,
+      "dependencies": {
+        "@types/hast": "^3.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-from-html/node_modules/hastscript": {
+      "version": "8.0.0",
+      "resolved": "https://registry.npmjs.org/hastscript/-/hastscript-8.0.0.tgz",
+      "integrity": "sha512-dMOtzCEd3ABUeSIISmrETiKuyydk1w0pa+gE/uormcTpSYuaNJPbX1NU3JLyscSLjwAQM8bWMhhIlnCqnRvDTw==",
+      "dev": true,
+      "dependencies": {
+        "@types/hast": "^3.0.0",
+        "comma-separated-tokens": "^2.0.0",
+        "hast-util-parse-selector": "^4.0.0",
+        "property-information": "^6.0.0",
+        "space-separated-tokens": "^2.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
     "node_modules/hast-util-from-html/node_modules/parse5": {
       "version": "7.1.2",
+      "dev": true,
       "license": "MIT",
       "dependencies": {
         "entities": "^4.4.0"
@@ -5737,6 +5600,62 @@
         "url": "https://github.com/inikulin/parse5?sponsor=1"
       }
     },
+    "node_modules/hast-util-from-html/node_modules/unist-util-stringify-position": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/unist-util-stringify-position/-/unist-util-stringify-position-4.0.0.tgz",
+      "integrity": "sha512-0ASV06AAoKCDkS2+xw5RXJywruurpbC4JZSm7nr7MOt1ojAzvyyaO+UxZf18j8FCF6kmzCZKcAgN/yu2gm2XgQ==",
+      "dev": true,
+      "dependencies": {
+        "@types/unist": "^3.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-from-html/node_modules/vfile": {
+      "version": "6.0.1",
+      "resolved": "https://registry.npmjs.org/vfile/-/vfile-6.0.1.tgz",
+      "integrity": "sha512-1bYqc7pt6NIADBJ98UiG0Bn/CHIVOoZ/IyEkqIruLg0mE1BKzkOXY2D6CSqQIcKqgadppE5lrxgWXJmXd7zZJw==",
+      "dev": true,
+      "dependencies": {
+        "@types/unist": "^3.0.0",
+        "unist-util-stringify-position": "^4.0.0",
+        "vfile-message": "^4.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-from-html/node_modules/vfile-location": {
+      "version": "5.0.2",
+      "resolved": "https://registry.npmjs.org/vfile-location/-/vfile-location-5.0.2.tgz",
+      "integrity": "sha512-NXPYyxyBSH7zB5U6+3uDdd6Nybz6o6/od9rk8bp9H8GR3L+cm/fC0uUTbqBmUTnMCUDslAGBOIKNfvvb+gGlDg==",
+      "dev": true,
+      "dependencies": {
+        "@types/unist": "^3.0.0",
+        "vfile": "^6.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-from-html/node_modules/vfile-message": {
+      "version": "4.0.2",
+      "resolved": "https://registry.npmjs.org/vfile-message/-/vfile-message-4.0.2.tgz",
+      "integrity": "sha512-jRDZ1IMLttGj41KcZvlrYAaI3CfqpLpfpf+Mfig13viT6NKvRzWZ+lXz0Y5D60w6uJIBAOGq9mSHf0gktF0duw==",
+      "dev": true,
+      "dependencies": {
+        "@types/unist": "^3.0.0",
+        "unist-util-stringify-position": "^4.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
     "node_modules/hast-util-from-parse5": {
       "version": "7.1.2",
       "license": "MIT",
@@ -5845,16 +5764,18 @@
       }
     },
     "node_modules/hast-util-to-html": {
-      "version": "8.0.4",
+      "version": "9.0.0",
-      "license": "MIT",
+      "resolved": "https://registry.npmjs.org/hast-util-to-html/-/hast-util-to-html-9.0.0.tgz",
+      "integrity": "sha512-IVGhNgg7vANuUA2XKrT6sOIIPgaYZnmLx3l/CCOAK0PtgfoHrZwX7jCSYyFxHTrGmC6S9q8aQQekjp4JPZF+cw==",
       "dependencies": {
-        "@types/hast": "^2.0.0",
+        "@types/hast": "^3.0.0",
-        "@types/unist": "^2.0.0",
+        "@types/unist": "^3.0.0",
         "ccount": "^2.0.0",
         "comma-separated-tokens": "^2.0.0",
-        "hast-util-raw": "^7.0.0",
+        "hast-util-raw": "^9.0.0",
-        "hast-util-whitespace": "^2.0.0",
+        "hast-util-whitespace": "^3.0.0",
-        "html-void-elements": "^2.0.0",
+        "html-void-elements": "^3.0.0",
+        "mdast-util-to-hast": "^13.0.0",
         "property-information": "^6.0.0",
         "space-separated-tokens": "^2.0.0",
         "stringify-entities": "^4.0.0",
@@ -5865,6 +5786,204 @@
         "url": "https://opencollective.com/unified"
       }
     },
+    "node_modules/hast-util-to-html/node_modules/@types/hast": {
+      "version": "3.0.1",
+      "resolved": "https://registry.npmjs.org/@types/hast/-/hast-3.0.1.tgz",
+      "integrity": "sha512-hs/iBJx2aydugBQx5ETV3ZgeSS0oIreQrFJ4bjBl0XvM4wAmDjFEALY7p0rTSLt2eL+ibjRAAs9dTPiCLtmbqQ==",
+      "dependencies": {
+        "@types/unist": "*"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/@types/unist": {
+      "version": "3.0.0",
+      "resolved": "https://registry.npmjs.org/@types/unist/-/unist-3.0.0.tgz",
+      "integrity": "sha512-MFETx3tbTjE7Uk6vvnWINA/1iJ7LuMdO4fcq8UfF0pRbj01aGLduVvQcRyswuACJdpnHgg8E3rQLhaRdNEJS0w=="
+    },
+    "node_modules/hast-util-to-html/node_modules/hast-util-from-parse5": {
+      "version": "8.0.1",
+      "resolved": "https://registry.npmjs.org/hast-util-from-parse5/-/hast-util-from-parse5-8.0.1.tgz",
+      "integrity": "sha512-Er/Iixbc7IEa7r/XLtuG52zoqn/b3Xng/w6aZQ0xGVxzhw5xUFxcRqdPzP6yFi/4HBYRaifaI5fQ1RH8n0ZeOQ==",
+      "dependencies": {
+        "@types/hast": "^3.0.0",
+        "@types/unist": "^3.0.0",
+        "devlop": "^1.0.0",
+        "hastscript": "^8.0.0",
+        "property-information": "^6.0.0",
+        "vfile": "^6.0.0",
+        "vfile-location": "^5.0.0",
+        "web-namespaces": "^2.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/hast-util-parse-selector": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/hast-util-parse-selector/-/hast-util-parse-selector-4.0.0.tgz",
+      "integrity": "sha512-wkQCkSYoOGCRKERFWcxMVMOcYE2K1AaNLU8DXS9arxnLOUEWbOXKXiJUNzEpqZ3JOKpnha3jkFrumEjVliDe7A==",
+      "dependencies": {
+        "@types/hast": "^3.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/hast-util-raw": {
+      "version": "9.0.1",
+      "resolved": "https://registry.npmjs.org/hast-util-raw/-/hast-util-raw-9.0.1.tgz",
+      "integrity": "sha512-5m1gmba658Q+lO5uqL5YNGQWeh1MYWZbZmWrM5lncdcuiXuo5E2HT/CIOp0rLF8ksfSwiCVJ3twlgVRyTGThGA==",
+      "dependencies": {
+        "@types/hast": "^3.0.0",
+        "@types/unist": "^3.0.0",
+        "@ungap/structured-clone": "^1.0.0",
+        "hast-util-from-parse5": "^8.0.0",
+        "hast-util-to-parse5": "^8.0.0",
+        "html-void-elements": "^3.0.0",
+        "mdast-util-to-hast": "^13.0.0",
+        "parse5": "^7.0.0",
+        "unist-util-position": "^5.0.0",
+        "unist-util-visit": "^5.0.0",
+        "vfile": "^6.0.0",
+        "web-namespaces": "^2.0.0",
+        "zwitch": "^2.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/hast-util-to-parse5": {
+      "version": "8.0.0",
+      "resolved": "https://registry.npmjs.org/hast-util-to-parse5/-/hast-util-to-parse5-8.0.0.tgz",
+      "integrity": "sha512-3KKrV5ZVI8if87DVSi1vDeByYrkGzg4mEfeu4alwgmmIeARiBLKCZS2uw5Gb6nU9x9Yufyj3iudm6i7nl52PFw==",
+      "dependencies": {
+        "@types/hast": "^3.0.0",
+        "comma-separated-tokens": "^2.0.0",
+        "devlop": "^1.0.0",
+        "property-information": "^6.0.0",
+        "space-separated-tokens": "^2.0.0",
+        "web-namespaces": "^2.0.0",
+        "zwitch": "^2.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/hast-util-whitespace": {
+      "version": "3.0.0",
+      "resolved": "https://registry.npmjs.org/hast-util-whitespace/-/hast-util-whitespace-3.0.0.tgz",
+      "integrity": "sha512-88JUN06ipLwsnv+dVn+OIYOvAuvBMy/Qoi6O7mQHxdPXpjy+Cd6xRkWwux7DKO+4sYILtLBRIKgsdpS2gQc7qw==",
+      "dependencies": {
+        "@types/hast": "^3.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/hastscript": {
+      "version": "8.0.0",
+      "resolved": "https://registry.npmjs.org/hastscript/-/hastscript-8.0.0.tgz",
+      "integrity": "sha512-dMOtzCEd3ABUeSIISmrETiKuyydk1w0pa+gE/uormcTpSYuaNJPbX1NU3JLyscSLjwAQM8bWMhhIlnCqnRvDTw==",
+      "dependencies": {
+        "@types/hast": "^3.0.0",
+        "comma-separated-tokens": "^2.0.0",
+        "hast-util-parse-selector": "^4.0.0",
+        "property-information": "^6.0.0",
+        "space-separated-tokens": "^2.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/html-void-elements": {
+      "version": "3.0.0",
+      "resolved": "https://registry.npmjs.org/html-void-elements/-/html-void-elements-3.0.0.tgz",
+      "integrity": "sha512-bEqo66MRXsUGxWHV5IP0PUiAWwoEjba4VCzg0LjFJBpchPaTfyfCKTG6bc5F8ucKec3q5y6qOdGyYTSBEvhCrg==",
+      "funding": {
+        "type": "github",
+        "url": "https://github.com/sponsors/wooorm"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/parse5": {
+      "version": "7.1.2",
+      "resolved": "https://registry.npmjs.org/parse5/-/parse5-7.1.2.tgz",
+      "integrity": "sha512-Czj1WaSVpaoj0wbhMzLmWD69anp2WH7FXMB9n1Sy8/ZFF9jolSQVMu1Ij5WIyGmcBmhk7EOndpO4mIpihVqAXw==",
+      "dependencies": {
+        "entities": "^4.4.0"
+      },
+      "funding": {
+        "url": "https://github.com/inikulin/parse5?sponsor=1"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/unist-util-position": {
+      "version": "5.0.0",
+      "resolved": "https://registry.npmjs.org/unist-util-position/-/unist-util-position-5.0.0.tgz",
+      "integrity": "sha512-fucsC7HjXvkB5R3kTCO7kUjRdrS0BJt3M/FPxmHMBOm8JQi2BsHAHFsy27E0EolP8rp0NzXsJ+jNPyDWvOJZPA==",
+      "dependencies": {
+        "@types/unist": "^3.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/unist-util-stringify-position": {
+      "version": "4.0.0",
+      "resolved": "https://registry.npmjs.org/unist-util-stringify-position/-/unist-util-stringify-position-4.0.0.tgz",
+      "integrity": "sha512-0ASV06AAoKCDkS2+xw5RXJywruurpbC4JZSm7nr7MOt1ojAzvyyaO+UxZf18j8FCF6kmzCZKcAgN/yu2gm2XgQ==",
+      "dependencies": {
+        "@types/unist": "^3.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/vfile": {
+      "version": "6.0.1",
+      "resolved": "https://registry.npmjs.org/vfile/-/vfile-6.0.1.tgz",
+      "integrity": "sha512-1bYqc7pt6NIADBJ98UiG0Bn/CHIVOoZ/IyEkqIruLg0mE1BKzkOXY2D6CSqQIcKqgadppE5lrxgWXJmXd7zZJw==",
+      "dependencies": {
+        "@types/unist": "^3.0.0",
+        "unist-util-stringify-position": "^4.0.0",
+        "vfile-message": "^4.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/vfile-location": {
+      "version": "5.0.2",
+      "resolved": "https://registry.npmjs.org/vfile-location/-/vfile-location-5.0.2.tgz",
+      "integrity": "sha512-NXPYyxyBSH7zB5U6+3uDdd6Nybz6o6/od9rk8bp9H8GR3L+cm/fC0uUTbqBmUTnMCUDslAGBOIKNfvvb+gGlDg==",
+      "dependencies": {
+        "@types/unist": "^3.0.0",
+        "vfile": "^6.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
+    "node_modules/hast-util-to-html/node_modules/vfile-message": {
+      "version": "4.0.2",
+      "resolved": "https://registry.npmjs.org/vfile-message/-/vfile-message-4.0.2.tgz",
+      "integrity": "sha512-jRDZ1IMLttGj41KcZvlrYAaI3CfqpLpfpf+Mfig13viT6NKvRzWZ+lXz0Y5D60w6uJIBAOGq9mSHf0gktF0duw==",
+      "dependencies": {
+        "@types/unist": "^3.0.0",
+        "unist-util-stringify-position": "^4.0.0"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
     "node_modules/hast-util-to-parse5": {
       "version": "7.1.0",
       "license": "MIT",
@@ -9313,6 +9432,28 @@
         "url": "https://opencollective.com/unified"
       }
     },
+    "node_modules/rehype-stringify/node_modules/hast-util-to-html": {
+      "version": "8.0.4",
+      "resolved": "https://registry.npmjs.org/hast-util-to-html/-/hast-util-to-html-8.0.4.tgz",
+      "integrity": "sha512-4tpQTUOr9BMjtYyNlt0P50mH7xj0Ks2xpo8M943Vykljf99HW6EzulIoJP1N3eKOSScEHzyzi9dm7/cn0RfGwA==",
+      "dependencies": {
+        "@types/hast": "^2.0.0",
+        "@types/unist": "^2.0.0",
+        "ccount": "^2.0.0",
+        "comma-separated-tokens": "^2.0.0",
+        "hast-util-raw": "^7.0.0",
+        "hast-util-whitespace": "^2.0.0",
+        "html-void-elements": "^2.0.0",
+        "property-information": "^6.0.0",
+        "space-separated-tokens": "^2.0.0",
+        "stringify-entities": "^4.0.0",
+        "zwitch": "^2.0.4"
+      },
+      "funding": {
+        "type": "opencollective",
+        "url": "https://opencollective.com/unified"
+      }
+    },
     "node_modules/rehype-stringify/node_modules/unified": {
       "version": "10.1.2",
       "license": "MIT",

package.json

@@ -33,6 +33,8 @@
   },
   "devDependencies": {
     "@types/lodash-es": "^4.17.9",
+    "hast-util-from-html": "^2.0.1",
+    "hast-util-to-html": "^9.0.0",
     "mdast": "^3.0.0",
     "mdast-util-from-markdown": "^2.0.0",
     "prettier": "^3.0.3",

plugin/remark-agda.ts

@@ -1,17 +1,21 @@
 import type { RemarkPlugin } from "@astrojs/markdown-remark";
+import type { Node, Root, Parent, RootContent } from "hast";
 import { fromMarkdown } from "mdast-util-from-markdown";
+import { fromHtml } from "hast-util-from-html";
+import { toHtml } from "hast-util-to-html";
 
 import { spawnSync } from "node:child_process";
 import { mkdtempSync, mkdirSync, readFileSync } from "node:fs";
 import { tmpdir } from "node:os";
 import { join, parse } from "node:path";
+import { visit } from "unist-util-visit";
 
 const remarkAgda: RemarkPlugin = () => {
   return function (tree, { data }) {
     const path: string = data.astro.fileURL.pathname;
     if (!(path.endsWith(".lagda.md") || path.endsWith(".agda"))) return;
 
-    console.log("data", data);
+    // console.log("data", data);
 
     const tempDir = mkdtempSync(join(tmpdir(), "agdaRender."));
     const outDir = join(tempDir, "output");
@@ -20,18 +24,13 @@ const remarkAgda: RemarkPlugin = () => {
 
     const childOutput = spawnSync(
       "agda",
-      [
+      ["--html", `--html-dir=${outDir}`, "--highlight-occurrences", "--html-highlight=code", path],
-        "--html",
-        `--html-dir=${outDir}`,
-        "--highlight-occurrences",
-        "--html-highlight=code",
-        data.astro.fileURL.pathname,
-      ],
       {},
     );
 
     console.log("output", childOutput.output.toString());
-    const filename = parse(path).base.replace(/\.lagda/, "");
+    const filename = parse(path).base.replace(/\.lagda.md/, ".md");
+    const htmlname = parse(path).base.replace(/\.lagda.md/, ".html");
     console.log();
     console.log("filename", filename);
 
@@ -41,13 +40,47 @@ const remarkAgda: RemarkPlugin = () => {
 
     const doc = readFileSync(fullOutputPath);
     const tree2 = fromMarkdown(doc);
-    console.log("tree", tree);
+    // console.log("tree", tree);
 
-    tree.children = tree2.children;
+    const collectedCodeBlocks: RootContent[] = [];
+    visit(tree2, "html", (node) => {
+      //   console.log("node", node);
+      //   collectedCodeBlocks.push
+      const html = fromHtml(node.value, { fragment: true });
 
-    // visit(tree, "", (node) => {
+      const firstChild: RootContent = html.children[0]!;
-    //   console.log("node", node);
+      console.log("child", firstChild);
-    // });
+
+      visit(html, "element", (node) => {
+        if (node.tagName !== "a") return;
+
+        if (node.properties.href && node.properties.href.includes(htmlname)) {
+          console.log("a", node.properties);
+          node.properties.href = node.properties.href.replace(htmlname, "");
+        }
+      });
+
+      if (!firstChild?.properties?.className?.includes("Agda")) return;
+
+      const stringContents = toHtml(firstChild);
+      //   console.log("result", stringContents);
+      collectedCodeBlocks.push({
+        contents: stringContents,
+      });
+    });
+
+    console.log("collected len", collectedCodeBlocks.length);
+
+    let idx = 0;
+    visit(tree, "code", (node) => {
+      if (node.lang !== "agda") return;
+
+      //   console.log("node", node);
+      node.type = "html";
+      node.value = collectedCodeBlocks[idx].contents;
+      idx += 1;
+    });
+    console.log("len", idx);
   };
 };