+ class='content {{ if (eq .Section "entries") }} entries{{- end -}} {{ if (eq .File.BaseFileName "search") }}searchPage{{- end -}}'>
{{- partial "header.html" . -}}
{{- block "main" . }}{{- end }}
{{- block "footerfiles" . }}{{- end }}
+
diff --git a/admin/site/themes/afp/layouts/shortcodes/statistics.html b/admin/site/themes/afp/layouts/shortcodes/statistics.html
--- a/admin/site/themes/afp/layouts/shortcodes/statistics.html
+++ b/admin/site/themes/afp/layouts/shortcodes/statistics.html
@@ -1,216 +1,216 @@
{{ len (where .Site.RegularPages "Section" "==" "entries") }}
- Articles
+ Entries
- {{ len $.Site.Taxonomies.authors }} Authors
+ {{ len $.Site.Taxonomies.authors }}
+ Authors
~{{ lang.NumFmt 0 (mul (math.Round (div .Site.Data.statistics.num_lemmas 100)) 100) }}
Lemmas
~{{ lang.NumFmt 0 (mul (math.Round (div .Site.Data.statistics.num_loc 100)) 100) }}
Lines of Code
Most used AFP articles:
{{- $Scratch := newScratch -}}
{{- range ((where site.RegularPages "Section" "entries").GroupByDate "2006" ).Reverse -}}
{{- $collection := . -}}
{{- $Scratch.Add "years" (slice .Key) -}}
{{- with $Scratch.Get "articles_year" -}}
{{- $lastYearArticleCount := index (last 1 .) 0 -}}
{{- $articleCount := len $collection.Pages -}}
{{- $Scratch.Add "articles_year" (slice (int (add $articleCount $lastYearArticleCount))) -}}
{{- else }}
{{- $Scratch.Add "articles_year" (slice (len .Pages)) -}}
{{- end }}
{{- end }}
{{- range (where site.RegularPages "Section" "entries").Reverse -}}
{{- $Scratch.Add "all_articles" (slice (printf "'%s'" .File.BaseFileName )) -}}
{{- end }}
Growth in number of articles:
Growth in lines of code:
Growth in number of authors:
Size of articles:
\ No newline at end of file
diff --git a/admin/site/themes/afp/static/js/scroll-spy.js b/admin/site/themes/afp/static/js/scroll-spy.js
--- a/admin/site/themes/afp/static/js/scroll-spy.js
+++ b/admin/site/themes/afp/static/js/scroll-spy.js
@@ -1,130 +1,130 @@
/**
* Scrollspy, inspired from bootstrap. Original license:
* --------------------------------------------------------------------------
* Bootstrap (v5.1.3): scrollspy.js
* Licensed under MIT (https://github.com/twbs/bootstrap/blob/main/LICENSE)
*
* --------------------------------------------------------------------------
*/
const EVENT_SPY_ACTIVATE = 'activate.spy'
const CLASS_ACTIVE = 'active'
const CLASS_SPY_LINK = 'spy-link'
/**
* Class definition
*/
class ScrollSpy {
constructor(element, target, offset = 10) {
ScrollSpy.instance = this
this._element = element
this._offset = offset
this._offsets = []
this._link_ids = []
this._active_id = null
this._scrollHeight = 0
this._target = target
window.onscroll = () => this._process()
this.refresh()
this._process()
}
refresh() {
this._clear()
this._offsets = []
this._link_ids = []
this._scrollHeight = this._getScrollHeight()
const targets = []
for (const link of document.getElementById(this._target).getElementsByClassName(CLASS_SPY_LINK)) {
// visible and has id
- if (link.id && link.style.display !== 'none') {
+ if (link.id && !is_collapsed(link)) {
const target_id = link.getAttribute('href').slice(1)
const target = document.getElementById(target_id)
if (target) {
const targetBCR = target.getBoundingClientRect()
if (targetBCR.width || targetBCR.height) {
targets.push([targetBCR.top + window.pageYOffset, link.id])
}
}
}
}
for (const item of targets.sort((a, b) => a[0] - b[0])) {
this._offsets.push(item[0])
this._link_ids.push(item[1])
}
}
// Private
_getScrollHeight() {
return window.scrollHeight || Math.max(
document.body.scrollHeight,
document.documentElement.scrollHeight
)
}
_process() {
const scrollTop = window.pageYOffset + this._offset
const scrollHeight = this._getScrollHeight()
const maxScroll = this._offset + scrollHeight - window.innerHeight
if (this._scrollHeight !== scrollHeight) {
this.refresh()
}
if (scrollTop >= maxScroll) {
const target_id = this._link_ids[this._link_ids.length - 1]
if (this._active_id !== target_id) {
this._activate(target_id)
}
return
}
if (this._active_id && scrollTop < this._offsets[0] && this._offsets[0] > 0) {
this._clear()
return
}
for (let i = this._offsets.length; i--;) {
const isActiveTarget = this._active_id !== this._link_ids[i] &&
scrollTop >= this._offsets[i] &&
(typeof this._offsets[i + 1] === 'undefined' || scrollTop < this._offsets[i + 1])
if (isActiveTarget) {
this._activate(this._link_ids[i])
}
}
}
_activate(link_id) {
this._clear()
this._active_id = link_id
const link = document.getElementById(link_id)
if (link) {
link.classList.add(CLASS_ACTIVE)
const event = new Event(EVENT_SPY_ACTIVATE)
event.relatedTarget = link
window.dispatchEvent(event)
}
}
_clear() {
if (this._active_id) {
const link = document.getElementById(this._active_id)
- if (link.classList.contains(CLASS_ACTIVE)) {
+ if (link && link.classList.contains(CLASS_ACTIVE)) {
link.classList.remove(CLASS_ACTIVE)
}
}
}
static instance
}
\ No newline at end of file
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,294 @@
/* constants */
const ID_THEORY_LIST = 'theories'
const CLASS_LOADER = 'loader'
const CLASS_ANIMATION = 'animation'
-const CLASS_COLLAPSIBLE = 'collapsible'
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 DEFAULT_NAVBAR_TYPE = 'fact'
+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 `/entries/${href_parts[1].toLowerCase()}/theories#${href_parts[2]}`
}
else return `${base_href}/${rel_href}`
}
function to_id(thy_name, ref) {
if (ref) return `${thy_name}.html#${ref}`
else return `${thy_name}.html`
}
+const to_svg_id = (thy_name) => `${thy_name}#svg`
const to_container_id = (thy_name) => `${thy_name}#container`
const to_collapsible_id = (thy_name) => `${thy_name}#collapsible`
const to_spinner_id = (thy_name) => `${thy_name}#spinner`
const to_nav_id = (thy_name) => `${thy_name}#nav`
const to_ul_id = (thy_name) => `${thy_name}#ul`
const of_ul_id = (id) => id.split('#').slice(0, -1).join('#')
const to_a_id = (thy_name) => `${thy_name}#a`
function set_query(attribute, value) {
const params = new URLSearchParams(window.location.search)
params.set(attribute, value)
- const fragment = window.location.hash.length > 1 ? window.location.hash: ''
+ const fragment = window.location.hash.length > 1 ? window.location.hash : ''
const new_url = `${window.location.origin}${window.location.pathname}?${params.toString()}${fragment}`
- if (history.pushState) window.history.pushState({path: new_url}, '', new_url)
+ if (history.pushState) window.history.pushState({ path: new_url }, '', new_url)
else window.location = new_url
}
function get_query(attribute) {
const params = new URLSearchParams(window.location.search)
return params.get(attribute)
}
/* 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(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 collapsible = document.getElementById(to_collapsible_id(thy_name))
-
- if (collapsible) open(collapsible)
- else {
- const container = document.getElementById(to_container_id(thy_name))
+ const container = document.getElementById(to_container_id(thy_name))
- if (container) {
+ if (container) {
+ if (document.getElementById(to_collapsible_id(thy_name))) open(container)
+ else {
const collapsible = parse_elem(`
-
`)
+
`)
container.appendChild(collapsible)
+ open(container)
let refs = await load_theory(thy_name, container.getAttribute(ATTRIBUTE_THEORY_SRC))
await load_theory_nav(thy_name, refs)
const spinner = document.getElementById(to_spinner_id(thy_name))
spinner.parentNode.removeChild(spinner)
}
}
}
function nav_tree_rec(thy_name, path, key, ref_parts, type) {
const rec_ref = ref_parts.filter(e => e.length > 0)
const id = to_id(thy_name, `${path.join('.')}.${key}|${type}`)
let res
if (rec_ref.length < ref_parts.length) {
- res = `
${key} `
- } else res = `${key}`
+ res = `
${escape_html(key)} `
+ } else {
+ const head_id = to_id(thy_name, `${[...path, key, ...ref_parts[0]].join('.')}|${type}`)
+ res = `
${escape_html(key)} `
+ }
if (rec_ref.length > 1) {
const by_key = group_by(rec_ref)
const children = Object.keys(by_key).map((key1) => `
${nav_tree_rec(thy_name, [...path, key], key1, by_key[key1], type)} `)
return `
${res}
-
+ `
} else return res
}
function nav_tree(thy_name, refs, type) {
- let trees = Object.entries(group_by(refs)).map(([key, parts]) =>
+ let trees = Object.entries(group_by(refs || [])).map(([key, parts]) =>
`${nav_tree_rec(thy_name, [thy_name], key, parts, type)} `)
return parse_elem(`
-
+ `)
}
-const cached_refs = {}
+const cached_refs = Object.fromEntries(NAVBAR_TYPES.map(t => [t, {}]))
const load_theory_nav = (thy_name, refs) => {
- let selected = get_query(PARAM_NAVBAR_TYPE) ? get_query(PARAM_NAVBAR_TYPE) : DEFAULT_NAVBAR_TYPE
+ let selected = get_query(PARAM_NAVBAR_TYPE) || NAVBAR_TYPES[0]
let by_type = group_by(refs.filter(ref => ref.includes('|')).map((id) => id.split('|').reverse()))
let type_selector = document.getElementById(ID_NAVBAR_TYPE_SELECTOR)
let options = [...type_selector.options].map(e => e.value)
for (let [type, elems] of Object.entries(by_type)) {
- if (!options.includes(type)) type_selector.appendChild(parse_elem(`${type} `))
+ if (NAVBAR_TYPES.includes(type) && !options.includes(type)) {
+ type_selector.appendChild(parse_elem(`${type} `))
+ }
let parts_by_thy = group_by(elems.map((s) => s[0].split('.')))
- if (!cached_refs[type]) cached_refs[type] = {}
- cached_refs[type][thy_name] = parts_by_thy[thy_name]
+ if (NAVBAR_TYPES.includes(type)) cached_refs[type][thy_name] = parts_by_thy[thy_name]
}
let tree = nav_tree(thy_name, cached_refs[selected][thy_name], selected)
document.getElementById(to_nav_id(thy_name)).appendChild(tree)
ScrollSpy.instance.refresh()
}
-
/* state */
let navbar_last_opened = []
/* controls */
const follow_theory_hash = async () => {
let hash = window.location.hash
if (hash.length > 1) {
const id = hash.slice(1)
const thy_name = strip_suffix(id.split('#')[0], '.html')
await open_theory(thy_name)
const elem = document.getElementById(id)
if (elem) elem.scrollIntoView()
}
}
const toggle_theory = async (thy_name) => {
const hash = `#${to_id(thy_name)}`
- const collapsible = document.getElementById(to_collapsible_id(thy_name))
+ const collapsible = document.getElementById(to_container_id(thy_name))
if (collapsible) {
- if (!close(collapsible)) {
+ if (!collapse(collapsible)) {
if (window.location.hash === hash) open(collapsible)
else window.location.hash = hash
}
} else window.location.hash = hash
}
const change_selector = (type) => {
let old_type = get_query(PARAM_NAVBAR_TYPE)
if (!old_type || old_type !== type) {
set_query(PARAM_NAVBAR_TYPE, type)
for (const elem of document.getElementsByClassName(CLASS_NAVBAR_TYPE)) {
let thy_name = of_ul_id(elem.id)
elem.replaceWith(nav_tree(thy_name, cached_refs[type][thy_name], type))
}
ScrollSpy.instance.refresh()
}
}
const open_tree = (elem) => {
if (elem.classList.contains(CLASS_COLLAPSIBLE)) {
if (open(elem)) navbar_last_opened.push(elem)
}
if (elem.parentElement) open_tree(elem.parentElement)
}
const sync_navbar = (link) => {
for (const elem of navbar_last_opened){
- close(elem)
+ collapse(elem)
}
open_tree(link.parentElement)
- link.scrollIntoView()
+ link.scrollIntoView({block: "center"})
}
/* setup */
const init = async () => {
const theory_list = document.getElementById(ID_THEORY_LIST)
const navbar = document.getElementById(ID_NAVBAR)
if (theory_list && navbar) {
const thy_names = []
for (const theory of theory_list.children) {
thy_names.push(theory.id)
const href = theory.getAttribute('href')
const thy_name = theory.id
const thy_collapsible = parse_elem(`
-
+
`)
theory.replaceWith(thy_collapsible)
}
- const type = get_query(PARAM_NAVBAR_TYPE) ? get_query(PARAM_NAVBAR_TYPE) : DEFAULT_NAVBAR_TYPE
+ const type = get_query(PARAM_NAVBAR_TYPE) ? get_query(PARAM_NAVBAR_TYPE) : NAVBAR_TYPES[0]
navbar.appendChild(parse_elem(`
${type}
`))
navbar.append(...thy_names.map((thy_name) => parse_elem(`
${thy_name}
`)), parse_elem('
'))
window.onhashchange = follow_theory_hash
window.addEventListener(EVENT_SPY_ACTIVATE, (e) => sync_navbar(e.relatedTarget))
- new ScrollSpy(document.body, 'theory-navbar')
+ new ScrollSpy(document.body, ID_NAVBAR)
await follow_theory_hash()
}
}
document.addEventListener('DOMContentLoaded', init)
diff --git a/admin/site/themes/afp/static/js/util.js b/admin/site/themes/afp/static/js/util.js
--- a/admin/site/themes/afp/static/js/util.js
+++ b/admin/site/themes/afp/static/js/util.js
@@ -1,41 +1,68 @@
+
/* utilities */
+const CLASS_COLLAPSED = 'collapsed'
+const CLASS_COLLAPSIBLE = 'collapsible'
+const CLASS_INVERTIBLE = 'invertible'
+const CLASS_COLLAPSE_CONTAINER = 'collapse-container'
+
const strip_suffix = (str, suffix) => {
if (str.endsWith(suffix)) return str.slice(0, -suffix.length)
else return str
}
const group_by = (elems) => {
return elems.reduce((ks, kv) => {
if (kv.isEmpty) return ks
else {
const k = kv[0]
const vs = kv.slice(1)
if (ks[k]) ks[k].push(vs)
else ks[k] = [vs]
return ks
}
}, {})
}
const parse_elem = (html_str) => {
const template = document.createElement('template')
template.innerHTML = html_str
return template.content
}
+const is_collapsed = (e) => {
+ return e.classList.contains(CLASS_COLLAPSED)
+}
+
const open = (collapsible) => {
- if (collapsible.style.display === 'none') {
- collapsible.style.display = 'block'
+ if (collapsible.classList.contains(CLASS_COLLAPSED)) {
+ collapsible.classList.remove(CLASS_COLLAPSED)
return true
}
else return false
}
-const close = (collapsible) => {
- if (collapsible.style.display === 'block') {
- collapsible.style.display = 'none'
+const collapse = (collapsible) => {
+ if (!collapsible.classList.contains(CLASS_COLLAPSED)) {
+ collapsible.classList.add(CLASS_COLLAPSED)
return true
}
else return false
}
+
+const escape_html = (html) => {
+ return html.replace(/[&<>"']/g, function(m) {
+ switch (m) {
+ case '&':
+ return '&'
+ case '<':
+ return '<'
+ case '>':
+ return '>'
+ case '"':
+ return '"'
+ case "'":
+ return '''
+ }
+ })
+}
\ No newline at end of file
+