From 3935a8934c6aba1b8cc99861741eed7b38e748b2 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Wed, 11 Oct 2023 12:47:18 -0500 Subject: [PATCH] agda fix --- astro.config.ts | 12 +- package-lock.json | 681 +++++++++++++++++++++++++----------------- package.json | 2 + plugin/remark-agda.ts | 61 +++- 4 files changed, 470 insertions(+), 286 deletions(-) diff --git a/astro.config.ts b/astro.config.ts index c45a5a4..1e92afd 100644 --- a/astro.config.ts +++ b/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, + ], }, }); diff --git a/package-lock.json b/package-lock.json index 2cca0b5..584aa82 100644 --- a/package-lock.json +++ b/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", - "license": "MIT", + "version": "2.0.1", + "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", - "hast-util-from-parse5": "^7.0.0", + "@types/hast": "^3.0.0", + "devlop": "^1.1.0", + "hast-util-from-parse5": "^8.0.0", "parse5": "^7.0.0", - "vfile": "^5.0.0", - "vfile-message": "^3.0.0" + "vfile": "^6.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", - "license": "MIT", + "version": "9.0.0", + "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/unist": "^2.0.0", + "@types/hast": "^3.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-whitespace": "^2.0.0", - "html-void-elements": "^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", @@ -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", diff --git a/package.json b/package.json index b876d7d..e398d28 100644 --- a/package.json +++ b/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", diff --git a/plugin/remark-agda.ts b/plugin/remark-agda.ts index 2513944..f7e498f 100644 --- a/plugin/remark-agda.ts +++ b/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", - data.astro.fileURL.pathname, - ], + ["--html", `--html-dir=${outDir}`, "--highlight-occurrences", "--html-highlight=code", path], {}, ); 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) => { - // console.log("node", node); - // }); + const firstChild: RootContent = html.children[0]!; + 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); }; };