diff --git a/admin/site/config.json b/admin/site/config.json
--- a/admin/site/config.json
+++ b/admin/site/config.json
@@ -1,59 +1,60 @@
{
"baseURL": "/",
"languageCode": "en-gb",
"title": "Archive of Formal Proofs",
"theme": "afp",
"publishDir": "..",
"taxonomies": {
"author": "authors",
"topic": "topics",
"dependency": "dependencies"
},
"params": {
"description": "A collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle.",
"images": [
"/images/afp.png"
],
"title": "Archive of Formal Proofs",
"mainSections": ["entries"],
"afpUrls": {
"html": "https://www.isa-afp.org/browser_info/current/AFP",
"htmlDevel": "https://devel.isa-afp.org/browser_info/current/AFP"
}
},
"markup": {
"goldmark": {
"renderer": {
"unsafe": true
}
}
},
"menu": {
"main": [
{
"name": "Topics",
"url": "/topics/",
"weight": 2
}
]
},
"outputs": {
"home": ["html", "rss", "json"],
"taxonomyTerm": ["html", "json"]
},
"related": {
"includeNewer": true,
"indices": [
{
"name": "topics",
"weight": 1
},
{
"name": "keywords",
"weight": 3
}
],
"threshold": 80,
"toLower": true
- }
+ },
+ "relativeURLs": true
}
\ No newline at end of file
diff --git a/admin/site/themes/afp/assets/sass/main.scss b/admin/site/themes/afp/assets/sass/main.scss
--- a/admin/site/themes/afp/assets/sass/main.scss
+++ b/admin/site/themes/afp/assets/sass/main.scss
@@ -1,1107 +1,1136 @@
//colors
$theme: hsl(242, 27%, 24%);
$theme-hover: hsl(241, 26%, 36%);
$theme-lightest: hsl(261, 36%, 86%);
$theme-focus: #acabcf;
$link: #0645ad;
$link-hover: #0000ee;
$link-visited: #42047c;
$white: #fff;
$lightest-grey: #f2f2f2;
$lighter-grey: #ddd;
$light-grey: #bbb;
$dark-grey: #777;
$darker-grey: #555;
$darkest-grey: #303030;
$black: #000;
$black_15: rgba(0, 0, 0, 0.15);
//fonts
$sans-serif: "Open Sans", sans-serif;
$monospace: "Consolas", monospace;
$OpenSans: "Open Sans";
$light: 300;
$normal: 400;
$bold: 700;
$border-bottom: 2px $darker-grey solid;
//sizes
$size-xs: 650px; // for example mobile
$size-s: 875px; // for example half desktop window
$size-xl: 1800px; // for example 4k desktop
%code {
font-family: $monospace;
background-color: $lightest-grey;
color: $darkest-grey;
}
%button {
border: 1px solid $dark-grey;
font-size: 1rem;
vertical-align: middle;
background-color: $white;
color: $black;
line-height: 0;
font-family: $sans-serif;
}
%button-image {
position: relative;
top: 0.12em;
left: 5px;
padding-right: 5px;
}
%sticky {
- position: sticky;
- top: 0;
- background-color: $white;
- margin: 0;
- padding-bottom: 0.5rem;
+ position: sticky;
+ top: 0;
+ background-color: $white;
+ margin: 0;
+ padding-bottom: 0.5rem;
}
@font-face {
font-family: $OpenSans;
font-display: swap;
font-style: normal;
font-weight: 300;
src: local(""), url("/font/open-sans-v18-latin-300.woff2") format("woff2"),
url("/font/open-sans-v18-latin-300.woff") format("woff");
}
@font-face {
font-family: $OpenSans;
font-display: swap;
font-style: normal;
font-weight: 400;
src: local(""), url("/font/open-sans-v18-latin-regular.woff2") format("woff2"),
url("/font/open-sans-v18-latin-regular.woff") format("woff");
}
@font-face {
font-family: $OpenSans;
font-display: swap;
font-style: italic;
font-weight: 400;
src: local(""), url("/font/open-sans-v18-latin-italic.woff2") format("woff2"),
url("/font/open-sans-v18-latin-italic.woff") format("woff");
}
@font-face {
font-family: $OpenSans;
font-display: swap;
font-style: normal;
font-weight: 700;
src: local(""), url("/font/open-sans-v18-latin-700.woff2") format("woff2"),
url("/font/open-sans-v18-latin-700.woff") format("woff");
}
@font-face {
font-family: $OpenSans;
font-display: swap;
font-style: italic;
font-weight: 700;
src: local(""), url("/font/open-sans-v18-latin-700italic.woff2") format("woff2"),
url("/font/open-sans-v18-latin-700italic.woff") format("woff");
}
*::selection {
background-color: $theme;
color: $white;
}
body {
color: $black;
background: $white;
font-family: $sans-serif;
display: grid;
grid-template-columns: #{"max(20%, 200px)"} 1fr;
grid-template-areas: "sidebar content";
justify-items: center;
margin: 0;
}
aside {
grid-area: sidebar;
background-color: $theme;
width: 20vw;
margin: 0;
height: 100%;
position: fixed;
top: 0;
left: 0;
min-width: 200px;
word-break: break-all;
overflow-y: auto;
color: $white;
nav {
display: flex;
flex-direction: column;
justify-content: space-between;
height: 100vh;
}
ul {
list-style: none;
padding: 0;
}
li {
padding: 0.5em 2rem;
&:hover {
background-color: $theme-hover;
}
}
.active {
background-color: $theme-hover;
}
div > a {
display: block;
text-align: center;
}
a:not(.entity_ref) {
&:link,
&:visited {
color: $white;
}
&:focus {
outline: 1px $theme-focus solid;
outline-offset: 3.5px;
}
}
hr {
margin: 2rem;
border: none;
border-top: 2px solid $dark-grey;
}
}
.logo {
width: 40%;
height: auto;
padding: 10%;
max-width: 160px;
}
li {
margin: 0.25em 0;
}
header {
border-bottom: $border-bottom;
margin-bottom: 20px;
padding: 0.5rem 0;
> div {
display: flex;
justify-content: space-between;
padding: 0.5rem 0;
}
form {
padding: 0.5rem 0;
float: right;
}
h1 {
padding: 0.5rem 0;
margin: 0;
clear: both;
line-height: 2.75rem;
}
#search-input {
height: 2rem;
padding: 7px;
width: 175px;
}
#search-button {
height: 2rem;
padding: 7px;
width: 2rem;
&:hover {
background-color: $lighter-grey;
}
&:active {
background-color: $light-grey;
}
}
div p {
margin: 0;
}
}
.content {
grid-area: content;
margin: 0 auto 2rem;
width: #{"min(80%, 1100px)"};
min-width: 550px;
div {
line-height: 1.35em;
width: 100%;
h1 {
border-bottom: $border-bottom;
}
}
> div {
form {
margin: 2rem auto 0;
width: 50%;
min-width: 290px;
padding: 1rem 0;
}
#search-button {
height: 2.5rem;
width: 25%;
min-width: 70px;
background: $theme;
color: $white;
border: 1px $theme solid;
}
#search-input {
height: 2.5rem;
width: 75%;
}
}
.popup {
background: $white;
box-shadow: 0 0 8px 0 $black_15, 0 4px 10px 0 $black_15;
padding: 2.5rem;
display: block;
width: auto;
min-width: 300px;
max-width: 90vw;
max-height: 75vh;
position: fixed;
left: 50%;
top: 50%;
transform: translate(-50%, -50%);
overflow-y: auto;
}
.chart {
min-width: 400px;
width: 100%;
min-height: 400px;
max-height: 50vh;
background: $white;
margin: 20px auto 40px;
border: 1px solid $black;
position: relative;
}
.statsnumber {
text-align: right;
padding-right: 1rem;
}
ul {
list-style-type: none;
}
li {
word-wrap: break-word;
word-break: break-word;
}
li::before {
content: "–";
position: absolute;
margin-left: -1.3em;
}
}
.entries {
> div {
display: grid;
grid-template-columns: 3fr 1fr;
}
main {
padding-right: 2%;
max-width: 90ch;
div {
margin: 1rem 0;
}
}
nav {
width: 130px;
margin-left: auto;
h4 {
color: $darker-grey;
font-weight: $normal;
}
}
}
.theories {
grid-template-columns: 20% 80%;
justify-content: normal;
.collapsible.collapsed {
display: none;
}
.invertible.collapsed {
- transform: scale(1,-1);
+ transform: scale(1, -1);
}
.collapse-container.collapsed {
.collapsible {
display: none;
}
+
.invertible {
- transform: scale(1,-1);
+ transform: scale(1, -1);
}
}
.content {
- min-width: clamp(60ch,50vw,50vw);
+ min-width: clamp(60ch, 50vw, 50vw);
width: 100%;
max-width: 75vw;
margin: 0 0 2rem 4vw;
}
pre {
width: fit-content;
}
h2 {
@extend %sticky;
padding-top: 0.5rem;
border-bottom: 1px $light-grey solid;
svg {
height: 2rem;
width: 20px;
position: sticky;
right: 1rem;
float: right;
stroke: $dark-grey;
transition: transform 100ms;
}
}
main {
- > div {
- margin-bottom: 1rem;
- }
+ > div {
+ margin-bottom: 1rem;
+ }
}
aside {
word-break: normal;
z-index: 1;
overflow-x: hidden;
.logo {
- padding-top: 2rem;
- padding-bottom: 2rem;
- width: 100px;
+ padding-top: 2rem;
+ padding-bottom: 2rem;
+ width: 100px;
- @media screen and (min-width: $size-xl) {
- width: 150px;
- }
+ @media screen and (min-width: $size-xl) {
+ width: 150px;
+ }
+ }
+
+ #return {
+ position: sticky;
+ top: 0rem;
+ background: #2E2D4E;
+ min-width: 200px;
+ }
+
+ #pdfs {
+ position: fixed;
+ bottom: 0;
+ background: #2E2D4E;
+ margin: 0;
+ padding: 1rem 1.75rem;
+ width: 20vw;
+ box-sizing: border-box;
+ cursor: pointer;
}
> div {
margin-right: 1rem;
}
&:hover {
min-width: fit-content;
+
div {
min-width: fit-content;
}
- }
+ }
ul {
margin-left: 1.75rem;
}
li {
padding: 0;
&:hover {
background-color: $theme;
}
> a:hover {
background-color: $theme-hover;
}
a {
padding: 0.5em 0;
display: inline-block;
width: 100%;
}
}
}
@media screen and (max-width: $size-s) {
padding: 0;
grid-template-columns: 1fr;
+ aside {
+ overflow-x: visible;
+ }
+
+ #menu {
+ min-width: fit-content;
+ padding-right: 1rem;
+ }
+
.content {
min-width: 350px;
max-width: 100vw;
margin: 80px 0 0 20px;
}
h2 {
- top: 60px;
- }
-
- nav {
- display: none;
+ top: 80px;
+ padding-left: 0.5rem;
}
}
}
.links {
button {
display: inline-block;
margin: 0.5rem 0;
}
a {
display: inline-block;
margin: 0.5rem 0;
}
}
.popup-button:not(.entity_ref) {
&:visited {
color: $white;
}
&:link {
border: none;
padding: 0.75rem 0;
background-color: $theme;
color: $white;
cursor: pointer;
text-align: center;
transition: background-color 200ms ease, transform 150ms ease;
font-weight: $bold;
font-size: 0.9rem;
width: 130px;
}
&:active {
transform: scale(0.98);
}
}
a:not(.entity_ref) {
&:link {
color: $link;
text-decoration: none;
font-weight: $bold;
}
&:visited {
color: $link-visited;
}
&:hover {
color: $link-hover;
}
}
h1 {
margin: 1.5em 0 0 0;
font-size: 2em;
padding-bottom: 20px;
span.first {
font-size: 2.3rem;
}
}
h2 {
margin: 1.5em 0 0 0;
padding: 0;
line-height: normal;
}
h3 {
margin: 1.5em 0 0 0;
font-stretch: normal;
font-size: larger;
padding: 0;
font-weight: $light;
&:first-child {
margin: 0.5rem 0 0 0;
}
}
h4 {
margin: 1.5em 0 0 0;
margin-bottom: 0.5ex;
font-weight: $bold;
}
.popup {
h2 {
margin-top: 0;
}
.close {
position: absolute;
width: 20px;
height: 20px;
top: 2rem;
right: 2rem;
transition: all 200ms;
font-size: 24px;
font-weight: $bold;
color: $darker-grey;
text-align: center;
&:hover {
color: $darkest-grey;
}
}
}
#download-popup {
a[download] {
display: block;
width: 154px;
margin: 2.5rem auto 0;
}
}
.year {
@extend %sticky;
padding-top: 2rem;
border-bottom: $border-bottom;
}
img {
max-width: 90%;
}
pre {
@extend %code;
padding: 1rem;
overflow: auto;
&.bibtex {
white-space: pre;
border-width: thin;
border-style: solid;
}
&.code {
white-space: pre;
padding: 10px 2px;
}
}
code {
padding: 1px 2px 2px;
@extend %code;
}
blockquote {
border: 2px solid $lighter-grey;
padding: 1rem 2rem;
margin: auto 0;
}
tr:nth-child(even) {
background-color: $lightest-grey;
}
.nobr {
white-space: nowrap;
}
.large-top-margin {
margin-top: 48px;
}
.search-page {
> div {
display: grid;
grid-template-columns: 3fr #{"max(25%, 175px)"};
grid-template-rows: 150px 1fr;
grid-template-areas:
"search search"
"entries sidebar";
}
form {
grid-area: search;
}
#search-main {
grid-area: entries;
padding-right: 2rem;
box-sizing: border-box;
}
#search-results {
> div {
position: relative;
margin: 1.5rem 0;
border-bottom: 2px $lighter-grey solid;
padding-bottom: 1.5rem;
}
div + div {
margin-top: 1rem;
}
.title,
.subtitle {
display: flex;
justify-content: space-between;
align-items: center;
}
.subtitle {
color: $dark-grey;
font-size: 0.875em;
> p {
margin: 0;
}
}
a[download] {
padding: 5px 7.5px;
flex-shrink: 0;
margin-left: 1em;
}
}
#search-sidebar {
grid-area: sidebar;
}
}
a[download] {
display: inline-block;
color: $black;
height: 22px;
padding: 4px 7px;
@extend %button;
&:focus {
outline: none;
box-shadow: 0 0 0 2px #c5c4ddbb;
}
&:hover,
&:active {
background-color: $light-grey;
color: $black;
}
+
&:after {
content: url("/images/download.svg");
@extend %button-image;
}
}
.entry {
display: flex;
align-items: center;
margin-top: 1.35rem;
a[download] {
position: absolute;
top: 0;
right: 0;
}
.date {
text-align: right;
width: 15%;
min-width: 6ch;
font-family: $monospace;
}
h5 {
font-size: initial;
display: initial;
}
}
.form-container {
width: 290px;
text-align: left;
}
#search-input {
@extend %button;
border-right: none;
font-family: $sans-serif;
padding: 0.5em;
}
#search-button:not(.entity_ref) {
@extend %button;
cursor: pointer;
&:focus {
outline: none;
box-shadow: 0 0 0 2px #c5c4ddbb;
}
img {
max-width: 1rem;
}
}
.entity_def.active {
background-color: $theme-focus;
}
button {
@extend %button;
height: 2rem;
padding: 7px;
font-weight: $bold;
cursor: pointer;
&:hover {
background-color: $lighter-grey;
}
&:active {
background-color: $light-grey;
}
&:focus {
outline: none;
box-shadow: 0 0 0 2px #c5c4ddbb;
}
}
button[copy] {
&:after {
content: url("/images/copy.svg");
@extend %button-image;
}
}
#search-input-autocomplete-list {
width: 214px;
position: absolute;
margin-bottom: 24px;
padding: 8px 0;
background-color: $white;
border: 1px solid $lighter-grey;
box-shadow: 0 2px 4px $black_15;
z-index: 1;
div {
width: auto;
padding: 8px 12px;
line-height: 16px;
cursor: pointer;
&:hover {
background: $lighter-grey;
}
}
}
.autocomplete-active {
background: $lighter-grey;
}
.item-text {
width: 85%;
}
.date {
color: $darker-grey;
font-size: 14px;
}
.overlay {
position: fixed;
top: 0;
bottom: 0;
left: 0;
right: 0;
background: $black_15;
transition: opacity 200ms;
visibility: hidden;
opacity: 0;
.cancel {
position: absolute;
width: 100%;
height: 100%;
cursor: pointer;
}
&:target {
visibility: visible;
opacity: 1;
}
}
.status-ok {
background-color: #00FF99;
padding: 8px;
}
.status-skipped {
background-color: #FFFF99;
padding: 8px;
}
.status-failed {
background-color: #DD2222;
padding: 8px;
}
iframe {
width: 100%;
height: 90vh;
}
.loader {
margin: 24px 24px 0 0;
height: 6px;
position: relative;
display: block;
background-color: $theme;
border-radius: 4px;
overflow: hidden;
.animation {
background-color: $light-grey;
&:before {
content: '';
position: absolute;
background-color: inherit;
top: 0;
left: 0;
bottom: 0;
will-change: left, right;
animation: loader 2s linear infinite;
}
}
}
@keyframes loader {
0% {
left: -20%;
right: 100%;
}
100% {
left: 100%;
right: -20%;
}
}
#menu-toggle {
input,
label {
display: none;
}
> .logo-link, img[alt="Search"] {
display: none;
}
> #menu {
- box-shadow: 0 .5rem 1rem rgba(0,0,0,.15);
+ box-shadow: 0 .5rem 1rem rgba(0, 0, 0, .15);
}
form {
display: none;
}
}
@media screen and (max-width: $size-xs) {
.content {
width: 90%;
min-width: 350px;
}
.search-page {
> div {
display: grid;
grid-template-columns: 1fr;
- grid-template-rows: 150px auto auto ;
+ grid-template-rows: 150px auto auto;
grid-template-areas:
'search'
'sidebar'
'entries';
}
}
}
@media screen and (max-width: $size-s) {
body {
grid-template-columns: 1fr;
grid-template-areas: 'content';
}
aside {
- height: 4rem;
+ height: 80px;
width: 100vw;
overflow-y: visible;
z-index: 1;
}
header {
form {
display: none;
}
}
.content {
margin-top: 80px;
}
.entries {
> div {
display: grid;
grid-template-rows: auto auto;
grid-template-columns: 1fr;
}
nav {
margin-left: 0;
}
}
-
+
.large-top-margin {
margin-top: 0;
}
#banner {
left: 0;
width: 100vw;
height: 75px;
p {
line-height: normal;
margin: 1rem;
}
}
#menu-toggle {
background: $theme;
display: block;
position: relative;
top: 0;
left: 0;
z-index: 1;
height: 80px;
user-select: none;
width: 100vw;
+
a {
text-decoration: none;
transition: color 0.3s ease;
}
+
.logo-link {
height: 3rem;
max-width: 50vw;
top: 1rem;
left: 0;
right: 0;
- margin-left: auto;
+ margin-left: auto;
margin-right: auto;
-
img {
padding: 0;
height: 3rem;
object-fit: contain;
}
}
.logo-link, input, label, a[href="/search"] {
display: block;
position: absolute;
z-index: 2;
}
input, label, a[href="/search"] {
width: 24px;
height: 24px;
top: 28px;
}
- input,label {
+ input, label {
left: 28px;
cursor: pointer;
}
a[href="/search"] {
right: 28px;
filter: invert(1);
}
a[href="/search"] img, label img {
width: 100%;
}
input {
opacity: 0;
+
&:checked {
~ nav {
left: 0;
}
}
}
-
+
label span {
- display: none;
+ display: none;
}
}
#menu {
- height: 100vh;
+ height: calc(100vh - 80px);
position: absolute;
top: 0;
- left: 0;
- padding-top: 80px;
+ margin-top: 80px;
box-sizing: border-box;
min-width: 200px;
width: 50vw;
max-width: 350px;
min-height: 355px;
background: $theme;
left: -100%;
transition: left 0.3s ease;
+ overflow-y: scroll;
.logo-link {
display: none;
}
}
}
diff --git a/admin/site/themes/afp/layouts/partials/theory-navigation.html b/admin/site/themes/afp/layouts/partials/theory-navigation.html
--- a/admin/site/themes/afp/layouts/partials/theory-navigation.html
+++ b/admin/site/themes/afp/layouts/partials/theory-navigation.html
@@ -1,32 +1,39 @@
{{- $entry_name := .File.BaseFileName -}}
{{- $site := . -}}
{{- $path := .Site.Params.afpUrls.html -}}
{{- if isset .Site.Data "status" -}}
{{- $path = .Site.Params.afpUrls.htmlDevel -}}
{{- end -}}
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,277 +1,278 @@
/* 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 `/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`
/* 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 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(`
`)
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 = `${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]) =>
`${nav_tree_rec(thy_name, [thy_name], key, parts, type)}`)
return parse_elem(`
`)
}
const cached_refs = Object.fromEntries(NAVBAR_TYPES.map(t => [t, {}]))
const load_theory_nav = (thy_name, refs) => {
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 (NAVBAR_TYPES.includes(type) && !options.includes(type)) {
type_selector.appendChild(parse_elem(``))
}
let parts_by_thy = group_by(elems.map((s) => s[0].split('.')))
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_container_id(thy_name))
if (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){
collapse(elem)
}
open_tree(link.parentElement)
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) : NAVBAR_TYPES[0]
navbar.appendChild(parse_elem(`
`))
navbar.append(...thy_names.map((thy_name) => parse_elem(`
${thy_name}
- `)), parse_elem('
'))
+ `)))
+ navbar.insertAdjacentElement('afterend', document.createElement('hr'));
window.onhashchange = follow_theory_hash
window.addEventListener(EVENT_SPY_ACTIVATE, (e) => sync_navbar(e.relatedTarget))
new ScrollSpy(document.body, ID_NAVBAR)
await follow_theory_hash()
}
}
document.addEventListener('DOMContentLoaded', init)
-