michael/remark-agda
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
Plugin for processing Literate Agda files with Remark https://www.npmjs.com/package/remark-agda
4 commits 1 branch 0 tags 53 KiB
TypeScript 98.5%
Shell 1.5%
Find a file
Michael Zhang 20bc60bb4c update some metadata
2024-09-12 19:55:19 -05:00
scripts works 2024-09-12 19:43:27 -05:00
src works 2024-09-12 19:43:27 -05:00
test works 2024-09-12 19:43:27 -05:00
.gitignore initial 2024-09-12 18:38:07 -05:00
biome.json initial 2024-09-12 18:38:07 -05:00
bun.lockb works 2024-09-12 19:43:27 -05:00
package.json update some metadata 2024-09-12 19:55:19 -05:00
README.md update some metadata 2024-09-12 19:55:19 -05:00
remark-agda.agda-lib initial 2024-09-12 18:38:07 -05:00
tsconfig.json works 2024-09-12 19:43:27 -05:00

README.md

remark-agda

This is a plugin that processes Literate Agda files that are written in Markdown, and replaces it with the HTML directly. This is useful for blogs where you want to do additional processing with remark, such as Katex or others.

This plugin has been extracted from the source code of my blog.

Installation

npm i remark-agda
pnpm add remark-agda
bun add remark-agda

Usage

const vfile = await read("/path/to/file.lagda.md");
await unified()
    .use(remarkParse)
    .use(remarkAgda, options)
    .use(remarkRehype, { allowDangerousHtml: true })
    .use(rehypeRaw)
    .use(rehypeStringify)
    .process(vfile);

Note:

  • Since this returns raw HTML, we need the allowDangerousHtml: true flag to remarkRehype as well as the rehypeRaw plugin to convert back.

Contact

Author: Michael Zhang

License: GPL-3.0

Send questions to ~mzhang/public-inbox@lists.sr.ht