{{- htmlUnescape .Title -}}
- {{- with .Params.authors -}}by {{ partial "authors.html" (dict "site" $site "authors" .) -}}{{- end -}}
{{- htmlUnescape .Title -}}
- {{- $entry := . -}}
- {{- with .Params.authors -}}by {{ partial "authors.html" (dict "site" $site "authors" . "affiliations" $entry.Params.affiliations) -}}{{- end -}}
{{- $value | safeHTML -}}
{{- end -}} {{- end -}} {{- $Scratch := newScratch -}} - {{- with .Params.dependencies -}} -
{{ if and (ne .Kind "home") (ne .File.TranslationBaseName "search") -}}
{{ end -}}
Please enter a search term above.
') if (data.length === 0) return parse_elem('No results.
') else { const end = data.length > NUM_MAX_MAIN_RESULTS ? '...' : '' const res = parse_elem(` ${data.slice(0, NUM_MAX_MAIN_RESULTS).map(entry => render_entry(entry)).join('')}${end}`) new Mark(res).mark(query) return res } } function render_results_shortlist(data, query) { if (!data) return '' if (data.length === 0) return parse_elem('No results
') else { const end = data.length > NUM_MAX_SIDE_RESULTS ? 'No results
') } /* input handling */ function debounce(callback, wait) { let timeout return (...args) => { clearTimeout(timeout) timeout = setTimeout(function () { callback.apply(this, args) }, wait) } } function handleSubmit(value) { if (typeof history.pushState !== 'undefined') { history.pushState({}, 'Search the Archive - ' + value, '?s=' + value) } } /* setup */ const init_search = async () => { const input = document.getElementById(ID_SEARCH_INPUT) const button = document.getElementById(ID_SEARCH_BUTTON) const entries_res = document.getElementById(ID_RESULTS_ENTRIES) const authors_res = document.getElementById(ID_RESULTS_AUTHORS) const topics_res = document.getElementById(ID_RESULTS_TOPICS) const search_query = get_query('s') if (search_query) input.value = search_query.replace('+', ' ') const index_data = await Promise.all([ fetch('/index.json'), fetch('/authors/index.json'), fetch('/topics/index.json'), fetch('/data/keywords.json') ]) const index_json = await Promise.all(index_data.map(r => r.json())) const indexes = build_indexes(...index_json) input.addEventListener('keydown', (event) => { switch (event.key) { case 'Enter': event.preventDefault() handleSubmit(event.target.value) } }) const run_local_search = (query) => { let res = {} if (query && query.length > 1) { add_suggestions(indexes['suggest'], query) res = local_search(indexes, query) } authors_res.replaceChildren(render_results_shortlist(res.authors, query)) topics_res.replaceChildren(render_results_shortlist(res.topics, query)) entries_res.replaceChildren(render_entries_results(res.entries, query)) MathJax.typeset() } input.addEventListener('keyup', (event) => { switch (event.key) { case 'Enter': case 'Up': case 'ArrowUp': case 'Down': case 'ArrowDown': case 'Left': case 'ArrowLeft': case 'Right': case 'ArrowRight': case 'Escape': break default: run_local_search(event.target.value) } }) button.addEventListener('click', () => handleSubmit(input.value)) if (input.value) run_local_search(input.value) input.focus() // findfacts const findfacts_res = document.getElementById(ID_RESULTS_FINDFACTS) const findfacts_index = await get_findfacts_index() const memoized_findfacts_search = memoize(findfacts_search) const run_findfacts_search = async (query) => { let res = {} if (query && query.length > 2) { findfacts_res.replaceChildren(parse_elem('...
')) res = await memoized_findfacts_search([findfacts_index, query]) } findfacts_res.replaceChildren(render_findfacts_results(res)) } input.addEventListener('keyup', debounce(async (event) => run_findfacts_search(event.target.value), 300)) if (input.value) await run_findfacts_search(input.value) } document.addEventListener('DOMContentLoaded', init_search) diff --git a/admin/site/themes/afp/static/js/theory.js b/admin/site/themes/afp/static/js/theory.js --- a/admin/site/themes/afp/static/js/theory.js +++ b/admin/site/themes/afp/static/js/theory.js @@ -1,287 +1,279 @@ /* constants */ const ID_THEORY_LIST = 'theories' const CLASS_LOADER = 'loader' const CLASS_ANIMATION = 'animation' const ATTRIBUTE_THEORY_SRC = 'theory-src' const CLASS_NAVBAR_TYPE = 'theory-navbar-type' const CLASS_THY_NAV = 'thy-nav' const PARAM_NAVBAR_TYPE = 'theory-navbar-type' const ID_NAVBAR_TYPE_SELECTOR = 'navbar-type-selector' const ID_NAVBAR = 'theory-navbar' const NAVBAR_TYPES = ['fact', 'type', 'const'] /* routing */ function target(base_href, rel_href) { const href_parts = rel_href.split('/') if (href_parts.length === 1) return `#${href_parts[0]}` else if (href_parts.length === 3 && href_parts[0] === '..' && href_parts[1] !== '..') { return `../${href_parts[1].toLowerCase()}/#${href_parts[2]}` } else return `${base_href}/../${rel_href}` } -function to_ref(thy_name, ref) { +function to_id(thy_name, ref) { if (ref) return `${thy_name}.html#${ref}` else return `${thy_name}.html` } -const to_id = (id) => `${id}#` +const to_fresh_id = (id) => `${id}#` const to_svg_id = (id) => `${id}#svg` const to_container_id = (id) => `${id}#container` const to_collapsible_id = (id) => `${id}#collapsible` const to_spinner_id = (id) => `${id}#spinner` const to_nav_id = (id) => `${id}#nav` const to_ul_id = (id) => `${id}#ul` const of_ul_id = (id) => id.split('#').slice(0, -1).join('#') const to_a_id = (id) => `${id}#a` /* document translation */ function translate(base_href, thy_name, thy_body) { const thy_refs = [...thy_body.getElementsByTagName('span')].map((span) => { let ref = span.getAttribute('id') if (ref) { - span.setAttribute('id', to_id(to_ref(thy_name, ref))) + span.setAttribute('id', to_fresh_id(to_id(thy_name, ref))) } return ref }).filter(e => e) for (const link of thy_body.getElementsByTagName('a')) { const rel_href = link.getAttribute('href') link.setAttribute('href', target(base_href, rel_href)) } return thy_refs } /* theory lazy-loading */ async function fetch_theory_body(href) { const html_str = await fetch(href).then((http_res) => { if (http_res.status !== 200) return Promise.resolve(`${http_res.statusText}`) else return http_res.text() }).catch((_) => { console.log(`Could not load theory at '${href}'. Redirecting...`) window.location.replace(href) }) const parser = new DOMParser() const html = parser.parseFromString(html_str, 'text/html') return html.getElementsByTagName('body')[0] } async function load_theory(thy_name, href) { const thy_body = await fetch_theory_body(href) const refs = translate(href, thy_name, thy_body) const collapse = document.getElementById(to_collapsible_id(thy_name)) collapse.append(...Array(...thy_body.children).slice(1)) return refs } async function open_theory(thy_name) { const container = document.getElementById(to_container_id(thy_name)) if (container) { if (document.getElementById(to_collapsible_id(thy_name))) open(container) else { const collapsible = parse_elem(`