2024-06-26 23:18:47 +00:00
|
|
|
import type { RootContent } from "hast";
|
2023-10-11 16:48:34 +00:00
|
|
|
import { fromMarkdown } from "mdast-util-from-markdown";
|
2023-10-11 17:47:18 +00:00
|
|
|
import { fromHtml } from "hast-util-from-html";
|
|
|
|
|
import { toHtml } from "hast-util-to-html";
|
2023-10-11 16:48:34 +00:00
|
|
|
|
|
|
|
|
import { spawnSync } from "node:child_process";
|
2024-06-27 05:22:46 +00:00
|
|
|
import {
|
|
|
|
|
mkdirSync,
|
|
|
|
|
mkdtempSync,
|
|
|
|
|
readFileSync,
|
2024-06-29 01:48:21 +00:00
|
|
|
existsSync,
|
2024-06-27 05:22:46 +00:00
|
|
|
readdirSync,
|
|
|
|
|
copyFileSync,
|
|
|
|
|
writeFileSync,
|
|
|
|
|
} from "node:fs";
|
2023-10-11 16:48:34 +00:00
|
|
|
import { tmpdir } from "node:os";
|
|
|
|
|
import { join, parse } from "node:path";
|
2023-10-11 17:47:18 +00:00
|
|
|
import { visit } from "unist-util-visit";
|
2024-06-27 05:22:46 +00:00
|
|
|
import type { RemarkPlugin } from "@astrojs/markdown-remark";
|
|
|
|
|
|
|
|
|
|
interface Options {
|
|
|
|
|
base: string;
|
|
|
|
|
outDir: string;
|
|
|
|
|
publicDir: string;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
|
|
|
|
|
const destDir = join(publicDir, "generated", "agda");
|
|
|
|
|
mkdirSync(destDir, { recursive: true });
|
2023-10-11 16:48:34 +00:00
|
|
|
|
2024-04-05 15:34:32 +00:00
|
|
|
return (tree, { history }) => {
|
2024-06-26 23:18:47 +00:00
|
|
|
const path: string = history[history.length - 1]!;
|
2023-10-11 16:48:34 +00:00
|
|
|
if (!(path.endsWith(".lagda.md") || path.endsWith(".agda"))) return;
|
|
|
|
|
|
2024-06-26 23:18:47 +00:00
|
|
|
console.log("AGDA:processing path", path);
|
|
|
|
|
|
2023-10-11 16:48:34 +00:00
|
|
|
const tempDir = mkdtempSync(join(tmpdir(), "agdaRender."));
|
2024-06-27 05:22:46 +00:00
|
|
|
const agdaOutDir = join(tempDir, "output");
|
2024-06-29 01:48:21 +00:00
|
|
|
const agdaOutFilename = parse(path).base.replace(/\.lagda.md/, ".md");
|
|
|
|
|
const agdaOutFile = join(agdaOutDir, agdaOutFilename);
|
2024-06-27 05:22:46 +00:00
|
|
|
mkdirSync(agdaOutDir, { recursive: true });
|
2023-10-11 16:48:34 +00:00
|
|
|
|
|
|
|
|
const childOutput = spawnSync(
|
|
|
|
|
"agda",
|
2024-04-05 15:34:32 +00:00
|
|
|
[
|
|
|
|
|
"--html",
|
2024-06-27 05:22:46 +00:00
|
|
|
`--html-dir=${agdaOutDir}`,
|
2024-04-05 15:34:32 +00:00
|
|
|
"--highlight-occurrences",
|
|
|
|
|
"--html-highlight=code",
|
|
|
|
|
path,
|
|
|
|
|
],
|
2023-10-11 16:48:34 +00:00
|
|
|
{},
|
|
|
|
|
);
|
|
|
|
|
|
2024-06-29 01:48:21 +00:00
|
|
|
if (childOutput.error || !existsSync(agdaOutFile)) {
|
|
|
|
|
throw new Error(
|
|
|
|
|
`Agda error:
|
|
|
|
|
|
|
|
|
|
Stdout:
|
|
|
|
|
${childOutput.stdout}
|
|
|
|
|
|
|
|
|
|
Stderr:
|
|
|
|
|
${childOutput.stderr}`,
|
|
|
|
|
{
|
|
|
|
|
cause: childOutput.error,
|
|
|
|
|
},
|
|
|
|
|
);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// // TODO: Handle child output
|
|
|
|
|
// console.error("--AGDA OUTPUT--");
|
|
|
|
|
// console.error(childOutput);
|
|
|
|
|
// console.error(childOutput.stdout?.toString());
|
|
|
|
|
// console.error(childOutput.stderr?.toString());
|
|
|
|
|
// console.error("--AGDA OUTPUT--");
|
2024-06-27 05:22:46 +00:00
|
|
|
|
|
|
|
|
const referencedFiles = new Set();
|
|
|
|
|
for (const file of readdirSync(agdaOutDir)) {
|
|
|
|
|
referencedFiles.add(file);
|
|
|
|
|
|
|
|
|
|
const fullPath = join(agdaOutDir, file);
|
|
|
|
|
const fullDestPath = join(destDir, file);
|
|
|
|
|
|
|
|
|
|
if (file.endsWith(".html")) {
|
|
|
|
|
const src = readFileSync(fullPath);
|
|
|
|
|
writeFileSync(
|
|
|
|
|
fullDestPath,
|
|
|
|
|
`
|
|
|
|
|
<!DOCTYPE html>
|
|
|
|
|
<html>
|
|
|
|
|
<head>
|
|
|
|
|
<link rel="stylesheet" href="${base}generated/agda/Agda.css" />
|
|
|
|
|
</head>
|
|
|
|
|
<body>
|
|
|
|
|
<pre class="Agda">
|
|
|
|
|
${src}
|
|
|
|
|
</pre>
|
|
|
|
|
</body>
|
|
|
|
|
</html>
|
|
|
|
|
`,
|
|
|
|
|
);
|
|
|
|
|
} else {
|
|
|
|
|
copyFileSync(fullPath, fullDestPath);
|
|
|
|
|
}
|
|
|
|
|
}
|
2024-06-27 00:17:01 +00:00
|
|
|
|
2023-10-11 17:47:18 +00:00
|
|
|
const htmlname = parse(path).base.replace(/\.lagda.md/, ".html");
|
2023-10-11 16:48:34 +00:00
|
|
|
|
2024-06-29 01:48:21 +00:00
|
|
|
const doc = readFileSync(agdaOutFile);
|
2024-06-26 23:18:47 +00:00
|
|
|
|
|
|
|
|
// This is the post-processed markdown with HTML code blocks replacing the Agda code blocks
|
2023-10-11 16:48:34 +00:00
|
|
|
const tree2 = fromMarkdown(doc);
|
|
|
|
|
|
2023-10-11 17:47:18 +00:00
|
|
|
const collectedCodeBlocks: RootContent[] = [];
|
|
|
|
|
visit(tree2, "html", (node) => {
|
|
|
|
|
const html = fromHtml(node.value, { fragment: true });
|
2023-10-11 16:48:34 +00:00
|
|
|
|
2023-10-11 17:47:18 +00:00
|
|
|
const firstChild: RootContent = html.children[0]!;
|
|
|
|
|
|
|
|
|
|
visit(html, "element", (node) => {
|
|
|
|
|
if (node.tagName !== "a") return;
|
|
|
|
|
|
2024-06-27 05:22:46 +00:00
|
|
|
if (node.properties.href) {
|
|
|
|
|
// Trim off end
|
|
|
|
|
const [href, hash, ...rest] = node.properties.href.split("#");
|
|
|
|
|
if (rest.length > 0) throw new Error("come look at this");
|
|
|
|
|
|
|
|
|
|
if (href === htmlname) node.properties.href = `#${hash}`;
|
|
|
|
|
|
|
|
|
|
if (referencedFiles.has(href)) {
|
|
|
|
|
node.properties.href = `${base}generated/agda/${href}${hash ? `#${hash}` : ""}`;
|
|
|
|
|
node.properties.target = "_blank";
|
|
|
|
|
}
|
2023-10-11 17:47:18 +00:00
|
|
|
}
|
|
|
|
|
});
|
|
|
|
|
|
|
|
|
|
if (!firstChild?.properties?.className?.includes("Agda")) return;
|
|
|
|
|
|
|
|
|
|
const stringContents = toHtml(firstChild);
|
|
|
|
|
collectedCodeBlocks.push({
|
|
|
|
|
contents: stringContents,
|
|
|
|
|
});
|
|
|
|
|
});
|
|
|
|
|
|
|
|
|
|
let idx = 0;
|
|
|
|
|
visit(tree, "code", (node) => {
|
2024-06-26 23:18:47 +00:00
|
|
|
if (!(node.lang === null || node.lang === "agda")) return;
|
2023-10-11 17:47:18 +00:00
|
|
|
|
|
|
|
|
node.type = "html";
|
|
|
|
|
node.value = collectedCodeBlocks[idx].contents;
|
|
|
|
|
idx += 1;
|
|
|
|
|
});
|
2023-10-11 16:48:34 +00:00
|
|
|
};
|
|
|
|
|
};
|
|
|
|
|
|
|
|
|
|
export default remarkAgda;
|
