PhD student interested in interactive theorem proving.
General Utilities
Tag Utilities
// create markdown with inline style
function inlinemd() {
const node = md.apply(null, arguments);
node.style.display = "inline";
return node;
}
// inline markdown with special support to write $...$ for inline latex and $$...$$ for block latex
function mdtex() {
const replacements = [
{
regex: /\$\$([^\$]*)\$\$/,
regexFn: id => () => id,
tag: tex.block
},
{
regex: /(?:^|[^\$])\$(?!\$)([^\$]+)\$(?!\$)/,
regexFn: id => match => `${match[0] === '$' ? '' : match[0]}${id}`,
tag: tex
}
];
// we need to replace latex entries first to avoid the md processor to exchange symbols in tex blocks
const toReplace = []; // collects the replacements that will need to be done
const id = DOM.uid("mdtex").id; // some unique id
// create placeholders for the latex templates
arguments[0] = arguments[0].map((arg, i) =>
replacements.reduce((arg, { regex, _ }, index) => {
const matches = matchAll(arguments[0].raw[i], new RegExp(regex, "g")); // match in raw string to avoid escaping
let match = matches.nextRaw();
while (match) {
toReplace.push({ match: match[1], replacementsIndex: index });
arg = arg.replace(
regex,
replacements[index].regexFn(`${id}-${toReplace.length - 1}-${index}`)
); // replace corresponding match in escaped string
match = matches.nextRaw();
}
return arg;
}, arg)
);
const node = inlinemd.apply(null, arguments); // do the markdown job
// revert the replacements for the latex blocks and insert the latex code
node.innerHTML = toReplace.reduce(
(html, { match, replacementsIndex }, index) =>
html.replace(
`${id}-${index}-${replacementsIndex}`,
_ => replacements[replacementsIndex].tag`${match}`.outerHTML
),
node.innerHTML
);
return node;
}
Purpose-built for displays of data
Observable is your go-to platform for exploring data and creating expressive data visualizations. Use reactive JavaScript notebooks for prototyping and a collaborative canvas for visual data exploration and dashboard creation.
