31:T1170,viewof urls = { const exampleFileURL = 'https://github.com/leanprover-community/mathlib/blob/9f0687c721823eafa6a58c1137afbc80302470dd/src/number_theory/bernoulli.lean'; const examplePRURL = 'https://github.com/leanprover-community/mathlib/pull/1716/'; const examplePRNumber = '1716'; const output = html``; const exampleSingle = html`${exampleFileURL}`; const examplePR = html`${examplePRURL}`; const exampleNumber = html`${examplePRNumber}`; const form = html`

${output}

Input one of the following:

a GitHub URL to a single Lean file (e.g. ${exampleSingle})
a GitHub URL to a PR involving .lean files (e.g. ${examplePR})
a mathlib PR number (e.g. ${exampleNumber})

and then hit enter or unfocus the box. `; exampleSingle.onclick = () => { form.text.value = exampleFileURL; form.text.onchange(); }; examplePR.onclick = () => { form.text.value = examplePRURL; form.text.onchange(); }; exampleNumber.onclick = () => { form.text.value = examplePRNumber; form.text.onchange(); }; form.text.oninput = e => { e.stopPropagation(); }; function getUrlsFromPR(pr, repo, inputUrl) { // https://developer.github.com/v3/pulls/#list-pull-requests-files const ghUrl = `https://api.github.com/repos/${repo}/pulls/${pr}/files?per_page=100`; fetch(ghUrl) .then(res => { if (res.headers.has('link')) { // multiple pages! see https://developer.github.com/v3/guides/traversing-with-pagination/ const pages = parseInt( res.headers.get('link').match(/page=(\d+)>; rel="last"$/)[1] ); return res.json().then(async files => { const pageFiles = await Promise.all( Array.from({ length: pages - 1 }, (_, i) => fetch(ghUrl + `&page=${i + 2}`).then(res => res.json()) ) ); return [files, pageFiles].flat(2); }); } else return res.json(); }) .then(files => { if (files.message) { if (files.message === 'Not Found') output.value = `Could not find PR corresponding to: ${inputUrl}`; else output.value = files.message; form.text.style.backgroundColor = 'pink'; } else { form.value = files .map(({ blob_url }) => ({ url: blob_url, anchor: html`^` })) .filter(({ url }) => url.endsWith('.lean')); form.value.url = inputUrl; form.dispatchEvent(new CustomEvent('input')); form.text.style.backgroundColor = 'initial'; output.value = ''; } }) .catch(e => { output.value = e; form.text.style.backgroundColor = 'pink'; }); } form.text.onchange = () => { const value = form.text.value; if (value.startsWith('https://github.com/')) { if (value.match(/\/pull\//)) { const arr = value.split('/'); const repo = arr.slice(3, 5).join('/'); const pr = parseInt(arr[6]); getUrlsFromPR(pr, repo, arr.slice(0, 7).join('/')); } else { form.value = [{ url: value, anchor: html`^` }]; form.value.url = value; form.dispatchEvent(new CustomEvent('input')); form.text.style.backgroundColor = 'initial'; output.value = ''; } } else if (!isNaN(parseInt(value))) { getUrlsFromPR(parseInt(value), 'leanprover-community/mathlib', value); } else if (value.startsWith('https://gist.githubusercontent.com')) { form.value = [{ url: value, anchor: html`^` }]; form.value.url = value; form.dispatchEvent(new CustomEvent('input')); form.text.style.backgroundColor = 'initial'; output.value = ''; } else { output.value = `Could not parse "${value}" as a Lean file on GitHub, a PR on GitHub, or a number`; form.text.style.backgroundColor = 'pink'; } }; form.text.onchange(); form.onsubmit = e => e.preventDefault(); return form; }32:T481,viewof docs = { hljs; const mathMap = []; const docElement = html` ${files.map(({ url, file, anchor }) => { const { chunks, math } = leanFileParser(file); const element = md`

${anchor} ${url}

${chunks.map(({ type, line, doc }, i) => doc.trim().length > 0 ? md`

[<> line ${line}](${url}#L${line})${ type === 'Lean code' ? '' : `, ${type}` }:

${ type === 'docstring' || type === 'module docstring' ? doc.trim('\n') : `~~~lean ${doc.trim('\n')} ~~~` }

` : '' )}`; mathMap.push([element, math]); return element; })}`; docElement.value = mathMap; return docElement; }33:T635,function leanFileParser(input) { let { text, math } = removeMath(input, '$'); let currLine = 1; const chunks = []; function eatToNext(re) { const i = text.search(re); let eaten; if (i === -1) { eaten = text; text = ''; } else { eaten = text.slice(0, i); text = text.slice(i); } currLine += eaten.split('\n').length - 1; return eaten; } function eatBlockComment() { let nest = 1; let doc = ""; while (nest > 0) { doc += eatToNext(blockRE); if (text.slice(0, 2) === '/-') { nest++; doc += '/-'; } else { nest--; doc += nest > 0 ? '-/' : ''; } text = text.slice(2); } return doc; } const openCommentRE = new RegExp('/--|/-!'); const blockRE = new RegExp('/-|-/'); const closeCommentRE = new RegExp('-/'); let N = 0; while (text.length && ++N < 10000) { const line = currLine + 1; const doc = eatToNext(openCommentRE); chunks.push({ type: 'Lean code', line, doc }); text = text.slice(2); if (text[0] === '!') { text = text.slice(1); const line = currLine; const moduleDocString = eatBlockComment(); chunks.push({ type: 'module docstring', line, doc: moduleDocString }); } else if (text[0] === '-') { text = text.slice(1); const line = currLine; const docString = eatBlockComment(); chunks.push({ type: 'docstring', line, doc: docString }); } } return { chunks, math }; }34:T6ac,MathJax = { if (document.getElementById('mathjax')) { return window.MathJax; } let trigger; const ready = new Promise(res => (trigger = res)); // cf. https://github.com/leanprover-community/doc-gen/blob/master/print_docs.py#L279 window.MathJax = { tex: { inlineMath: [['$', '$']], displayMath: [['$$', '$$']] }, options: { skipHtmlTags: [ 'script', 'noscript', 'style', 'textarea', 'pre', 'code', 'annotation', 'annotation-xml', 'decl', 'decl_meta', 'attributes', 'decl_args', 'decl_header', 'decl_name', 'decl_type', 'equation', 'equations', 'structure_field', 'structure_fields', 'constructor', 'constructors', 'instances' ], ignoreHtmlClass: 'tex2jax_ignore', processHtmlClass: 'tex2jax_process' }, // http://docs.mathjax.org/en/latest/web/configuration.html#performing-actions-during-initialization startup: { ready: () => { // console.log('MathJax is loaded, but not yet initialized'); window.MathJax.startup.defaultReady(); trigger(); // console.log('MathJax is initialized, and the initial typeset is queued'); } } }; // http://docs.mathjax.org/en/latest/web/configuration.html#configuring-and-loading-in-one-script (function() { var script = document.createElement('script'); script.id = 'mathjax'; script.src = 'https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js'; script.async = true; document.head.appendChild(script); })(); await ready; return window.MathJax; }35:[] 2f:{"title":"GitHub Lean file viewer","cells":[{"id":0,"value":"md`# GitHub Lean file viewer\n\nView a [Lean](https://leanprover.github.io) file hosted on GitHub or view all changed Lean files in a PR to your favorite Lean repo!\n\nNote that getting the list of changed files from GitHub uses the GitHub API, and this is [rate-limited](https://developer.github.com/v3/#rate-limiting) to 60 requests per hour.\n\nFurther note that this page uses (a relatively old version of) the [\\`marked\\`](https://github.com/markedjs/marked) library to typeset markdown, so the results may differ from what you see on e.g. [the official mathlib doc page](https://leanprover-community.github.io/mathlib_docs/).`","pinned":false,"hidden":false,"mode":"ojs"},{"id":4,"value":"$31","pinned":false,"hidden":false,"mode":"ojs"},{"id":164,"value":"md`## [🔗 Permalink](${permalink({ url: urls.url })}#docs)\n------`","pinned":false,"hidden":false,"mode":"ojs"},{"id":380,"value":"toc = html`\n${viewof page}\n