viewof urls = { const output = html``; const exampleSingle = html`https://github.com/leanprover-community/mathlib/blob/master/src/geometry/manifold/manifold.lean`; const examplePR = html`https://github.com/leanprover-community/mathlib/pull/1716/`; const exampleNumber = html`1716`; 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 = 'https://github.com/leanprover-community/mathlib/blob/master/src/geometry/manifold/manifold.lean'; form.text.onchange(); }; examplePR.onclick = () => { form.text.value = 'https://github.com/leanprover-community/mathlib/pull/1716/'; form.text.onchange(); }; exampleNumber.onclick = () => { form.text.value = '1716'; 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'; } }) .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'; } } else if (!isNaN(parseInt(value))) { getUrlsFromPR(parseInt(value), 'leanprover-community/mathlib', 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; }