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,1088 +1,1088 @@
 //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;
 
 %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;
 }
 
 @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 {
+  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;
   }
 
-  #searchInput {
+  #search-input {
     height: 2rem;
     padding: 7px;
     width: 175px;
   }
 
-  #searchButton {
+  #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: 50vw;
   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;
     }
 
-    #searchButton {
+    #search-button {
       height: 2.5rem;
       width: 25%;
       min-width: 70px;
       background: $theme;
       color: $white;
       border: 1px $theme solid;
     }
 
-    #searchInput {
+    #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-break: break-all;
   }
 
   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);
   }
 
   .collapse-container.collapsed {
     .collapsible {
       display: none;
     }
     .invertible {
       transform: scale(1,-1);
     }
   }
 
   .content {
     min-width: clamp(80ch,50vw, 50vw);
     width: auto;
     max-width: 75vw;
     margin: 0 0 2rem 4vw;
   }
 
   h2 {
     @extend %sticky;
     padding-top: 0.5rem;
     border-bottom: 1px $light-grey solid;
 
     svg {
       height: 2rem;
       width: 20px;
       position: absolute;
       right: 1em;
       stroke: $dark-grey;
       transition: transform 100ms;
     }
   }
 
   main {
       > div {
           margin-bottom: 1rem;
       }
   }
 
   aside {
     word-break: normal;
     z-index: 1;
     overflow-x: hidden;
 
     .logo {
         padding-top: 2rem;
         padding-bottom: 2rem;
         width: 100px;
 
         @media (min-width: 1800px) {
             width: 150px;
         }
     }
 
     > 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 (max-width: 875px) {
     padding: 0;
     grid-template-columns: 1fr;
 
     .content {
       min-width: 350px;
       max-width: 100vw;
       margin: 80px 0;
     }
 
     nav {
       display: none;
     }
   }
 }
 
 .links {
   button {
     display: inline-block;
     margin: 0.5rem 0;
   }
 
   a {
     display: inline-block;
     margin: 0.5rem 0;
   }
 }
 
-.popUpButton {
+.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 {
+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;
     }
   }
 }
 
-#downloadPopUp {
+#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;
 }
 
-.largeTopMargin {
+.large-top-margin {
   margin-top: 48px;
 }
 
-.searchPage {
+.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;
 }
 
-#searchInput {
+#search-input {
   @extend %button;
   border-right: none;
   font-family: $sans-serif;
   padding: 0.5em;
 }
 
-#searchButton {
+#search-button:not(.entity_ref) {
   @extend %button;
   cursor: pointer;
 
   &:focus {
     outline: none;
     box-shadow: 0 0 0 2px #c5c4ddbb;
   }
 
   img {
     max-width: 1rem;
   }
 }
 
 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;
   }
 }
 
-#searchInputautocomplete-list {
+#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%;
   }
 }
 
-#menuToggle {
+#menu-toggle {
   input,
   label {
     display: none;
   }
 
-  > .logoLink, img[alt="Search"] {
+  > .logo-link, img[alt="Search"] {
     display: none;
   }
 
   > #menu {
     box-shadow: 0 .5rem 1rem rgba(0,0,0,.15);
   }
 
   form {
     display: none;
   }
 }
 
 @media (max-width: 650px) {
   .content {
     width: 90%;
     min-width: 350px;
   }
 
-  .searchPage {
+  .search-page {
     > div {
       display: grid;
       grid-template-columns: 1fr;
       grid-template-rows: 150px auto auto ;
       grid-template-areas:
         'search'
         'sidebar'
         'entries';
     }
   }
 }
 
 @media (max-width: 875px) {
   body {
     grid-template-columns: 1fr;
     grid-template-areas: 'content';
   }
 
   aside {
     height: 4rem;
     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;
     }
   }
 
     
-  .largeTopMargin {
+  .large-top-margin {
     margin-top: 0;
   }
 
   #banner {
     left: 0;
     width: 100vw;
     height: 75px;
 
     p {
       line-height: normal;
       margin: 1rem;
     }
   }
 
-  #menuToggle {
+  #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;
     }
-    .logoLink {
+    .logo-link {
       height: 3rem;
       max-width: 50vw;
       top: 1rem;
       left: 0;
       right: 0;
       margin-left: auto; 
       margin-right: auto;
 
 
       img {
         padding: 0;
         height: 3rem;
         object-fit: contain;
       }
     }
 
-    .logoLink, input, label, a[href="/search"] {
+    .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 { 
       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;
     }
   }
   #menu {
     height: 100vh;
     position: absolute;
     top: 0;
     left: 0;
     padding-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;
 
-    .logoLink {
+    .logo-link {
       display: none;
     }
   }
 }
diff --git a/admin/site/themes/afp/layouts/_default/baseof.html b/admin/site/themes/afp/layouts/_default/baseof.html
--- a/admin/site/themes/afp/layouts/_default/baseof.html
+++ b/admin/site/themes/afp/layouts/_default/baseof.html
@@ -1,24 +1,24 @@
 <!DOCTYPE html>
 <html lang="en">
 {{ partial "head.html" . }}
 
 <body class='mathjax_ignore {{ if (eq .Section "theories") }}theories{{- end -}}'>
   <aside>
     {{ if ne .Section "theories"}}
     {{- partial "navigation.html" . -}}
     {{ else }}
     {{- partial "theory-navigation.html" . -}}
     {{ end }}
   </aside>
 
   <div
-    class='content {{ if (eq .Section "entries") }} entries{{- end -}} {{ if (eq .File.BaseFileName "search") }}searchPage{{- end -}}'>
+    class='content {{ if (eq .Section "entries") }} entries{{- end -}} {{ if (eq .File.BaseFileName "search") }}search-page{{- end -}}'>
     {{- partial "header.html" . -}}
     <div>
       {{- block "main" . }}{{- end }}
       {{- block "footerfiles" . }}{{- end }}
     </div>
   </div>
 </body>
 
 </html>
\ No newline at end of file
diff --git a/admin/site/themes/afp/layouts/_default/search.html b/admin/site/themes/afp/layouts/_default/search.html
--- a/admin/site/themes/afp/layouts/_default/search.html
+++ b/admin/site/themes/afp/layouts/_default/search.html
@@ -1,29 +1,29 @@
 {{ define "footerfiles" }}
 <script src="/js/mark.min.js"></script>
 {{ end -}}
 
 {{- define "main" }}
 <form autocomplete="off" action="{{ "search" | absURL }}">
   <div class='form-container'>
-    <input id="searchInput" type="search" size="31" maxlength="255" value=""  aria-label="Search the AFP" list="autocomplete"><button id="searchButton"
+    <input id="search-input" type="search" size="31" maxlength="255" value=""  aria-label="Search the AFP" list="autocomplete"><button id="search-button"
       type="button">Search</button>
     <datalist id="autocomplete">
     </datalist>
   </div>
 </form>
 
 <div id="search-sidebar">
   <h3>Authors</h3>
   <div id="author-results"></div>
   <h3>Topics</h3>
   <div id="topic-results"></div>
   <h3>FindFacts Results</h3>
   <div id="find-facts-results"></div>
 </div>
 
 <div id="search-main">
   <h3>Entries</h3>
   <div id="search-results"></div>
 </div>
 
 {{ end }}
\ No newline at end of file
diff --git a/admin/site/themes/afp/layouts/entries/single.html b/admin/site/themes/afp/layouts/entries/single.html
--- a/admin/site/themes/afp/layouts/entries/single.html
+++ b/admin/site/themes/afp/layouts/entries/single.html
@@ -1,154 +1,154 @@
 {{- define "main" -}}
 {{- $site := . -}}
 {{- $path := .Site.Params.afpUrls.html -}}
 {{- if isset .Site.Data "status" -}}
   {{- $path = .Site.Params.afpUrls.htmlDevel -}}
 {{- end -}}
 {{- $entry_name := .File.BaseFileName -}}
 <main>
   {{- if isset .Site.Data "status" -}}
   <strong>
     This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.
   </strong>
   {{- end -}}
   <h3>Abstract</h3>
 
   <div class="abstract mathjax_process">{{- trim .Params.abstract "\n" | safeHTML -}}</div>
   {{- if (eq .Params.licence "BSD") -}}
   <a href="http://isa-afp.org/LICENSE">BSD License</a>
   {{- else if (eq .Params.license "LGPL") -}}
   <a href="http://isa-afp.org/LICENSE.LGPL">GNU Lesser General Public License (LGPL)</a>
   {{- else -}}
     {{- printf "%s License" .Params.license -}}
   {{- end -}}
 
   {{- with .Params.extra -}}
   {{- range $key, $value := . -}}
   <h3>{{- humanize $key -}}</h3>
 
   <p>{{- $value | safeHTML -}}</p>
   {{- end -}}
   {{- end -}}
 
   {{- $Scratch := newScratch -}}
   
   {{- with .Params.dependencies -}}
     <h3>Depends On</h3><ul>
       {{- range . -}}
       <li>{{- printf "[%s](/entries/%s.html)" . . | $.Page.RenderString -}}</li>
       {{- end -}}
     </ul>
   {{- end -}}
 
   {{- with (index .Site.Taxonomies.dependencies (urlize $entry_name)) -}}
     <h3>Used by</h3>
     <ul>
       {{- range . -}}
       <li>{{- printf "[%s](%s)" .File.BaseFileName .RelPermalink | $.Page.RenderString -}}</li>
       {{- end -}}
     </ul>
   {{- end -}}
 
   {{- with .Params.topics -}}
   <h3>Topics</h3>
   <ul>
     {{- range . -}}
     <li>{{- printf "[%s](/topics/%s)" . (urlize .) | $.Page.RenderString -}}</li>
     {{- end -}}
   </ul>
   {{- end -}}
 
   <h3>Theories</h3>
   <ul>
     {{ $file := printf "assets/theories/%s.html" $entry_name}}
     {{- with .Params.theories -}}
     {{- range . -}}
     <li>{{- printf "[%s](%s/theories#%s)" . (urlize $entry_name) . | $.Page.RenderString -}}</li>
     {{- end -}}
     {{- end -}}
   </ul>
 
   {{ $related := .Site.RegularPages.Related . | first 3 }}
   {{ with $related }}
   <h3>Related Entries</h3>
   <ul>
     {{ range . }}
     <li>{{- printf "[%s](%s)" .Title .RelPermalink | $.Page.RenderString -}}</li>
     {{ end }}
   </ul>
   {{ end }}
 </main>
 
 {{- if isset .Site.Data "status" -}}
   <nav>
   {{- $status := "none" -}}
   {{- range where .Site.Data.status.entries "entry" $entry_name -}}
     {{- $status = .status -}}
   {{- end -}}
     <div class="status-{{ $status }}">
       <p>Status: <strong>{{- $status -}}</strong></p>
       <p>{{ .Site.Data.status.build_data.time }}</p>
       <p>Isabelle/<wbr>{{ .Site.Data.status.build_data.isabelle_id }}</p>
       <p>AFP/<wbr>{{ .Site.Data.status.build_data.afp_id }}</p>
       <p><a href="{{ .Site.Data.status.build_data.url }}">{{ .Site.Data.status.build_data.job }}</a></p>
     </div>
   </nav>
 {{- else -}}
 <nav class='links'>
-  <a class='popUpButton' href="#citePopUp">Cite</a>
-  <a class='popUpButton' href="#downloadPopUp">Download</a>
+  <a class='popup-button' href="#citePopUp">Cite</a>
+  <a class='popup-button' href="#download-popup">Download</a>
   <h4>PDFs</h4>
   <a href="{{- $path -}}/{{- $entry_name -}}/outline.pdf">Proof
     outline</a>
   <a href="{{- $path -}}/{{- $entry_name -}}/document.pdf">Proof
     document</a>
   <a href="{{- $path -}}/{{- $entry_name -}}/session_graph.pdf">Dependencies</a>
 </nav>
 
 <div id="citePopUp" class="overlay">
   <a class="cancel" href="#"></a>
   <div class="popup">
     <h2>Cite</h2>
     <a class="close" href="#">&times;</a>
     <div>
       <p style="display:none;" id="bibtexFileName">{{- $entry_name -}}-AFP</p>
       <pre id="copyText">@article{{- "{" -}}{{- $entry_name -}}-AFP,
   author  = {{ "{" -}}{{- delimit .Params.authors ", " | replaceRE "(, )([^,]+$)" " and $2" -}}},
   title   = {{ "{" -}}{{- htmlUnescape .Params.title -}}},
   journal = {Archive of Formal Proofs},
   month   = {{ dateFormat "January" .Params.date -}},
   year    = {{ dateFormat "2006" .Params.date -}},
   note    = {\url{http://isa-afp.org/entries/{{- $entry_name -}}.html},
             Formal proof development},
   ISSN    = {2150-914x},
 }</pre>
       <button id="copyBibtex">Copy</button> <a id="downloadBibtex">Download</a>
     </div>
   </div>
 </div>
 
-<div id="downloadPopUp" class="overlay">
+<div id="download-popup" class="overlay">
   <a class="cancel" href="#"></a>
   <div class="popup">
     <h2>Download</h2>
     <a class="close" href="#">&times;</a>
     <a href="https://isa-afp.org/release/afp-{{- $entry_name -}}-current.tar.gz" download>Download latest</a>
     {{ with .Params.olderReleases -}}
     <p>Older releases:</p>
     <ul>
       {{- range $map := . -}}
       {{- range $key, $value := $map -}}
       <li>Isabelle {{- $key -}}:
         <a href="https://isa-afp.org/release/afp-{{- $entry_name -}}-{{- $value -}}.tar.gz">
           afp-{{- $entry_name -}}-{{- $value -}}.tar.gz
         </a>
       </li>
       {{- end -}}
       {{- end -}}
     </ul>
     {{- end }}
   </div>
 </div>
 {{- end -}}
 
 {{- end -}}
diff --git a/admin/site/themes/afp/layouts/index.html b/admin/site/themes/afp/layouts/index.html
--- a/admin/site/themes/afp/layouts/index.html
+++ b/admin/site/themes/afp/layouts/index.html
@@ -1,48 +1,48 @@
 {{- define "main" -}}
 <p>
   The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific
   developments,
   mechanically checked in the theorem prover <a href="http://isabelle.in.tum.de/">Isabelle</a>. It
   is organized in the way
   of a scientific journal, is indexed by <a href="http://dblp.uni-trier.de/db/journals/afp/">dblp</a> and has an
   ISSN:
   2150-914x. Submissions are refereed and we encourage companion AFP submissions to conference and journal
   publications. To cite an entry, please use the <a href="/help/#citing-entries">preferred citation style</a>.
 </p>
 
 {{- if isset .Site.Data "status" -}}
 <p>
 <strong>
 This is the development version of the archive, referring to a recent Isabelle development version.
 Some entries may not be in a working state.
 The main archive is available from the <a href="http://www.isa-afp.org/">front page</a>.
 </strong>
 </p>
 {{- end -}}
 
 <form autocomplete="off" action="{{ "search" | absURL }}">
   <div class='form-container'>
-    <input id="searchInput" type="search" size="31" maxlength="255" value="" aria-label="Search the AFP" list="autocomplete"><button
-      id="searchButton" type="button">Search</button>
+    <input id="search-input" type="search" size="31" maxlength="255" value="" aria-label="Search the AFP" list="autocomplete"><button
+      id="search-button" type="button">Search</button>
     <datalist id="autocomplete">
     </datalist>
   </div>
 </form>
 
 {{- range (where site.RegularPages "Type" "in" site.Params.mainSections).GroupByDate "2006" -}}
 <div>
   <h2 class="year">{{- .Key -}}</h2>
   {{- range .Pages }}
   <article class="entry">
     <div class="item-text">
       <h5><a class="title" href="{{ .RelPermalink }}">{{- htmlUnescape .Title -}}</a></h5> <br>
         by {{ partial "authors.html" (dict "site" . "authors" .Params.authors) -}}
     </div>
     <span class="date">
       {{ .Date.Format "Jan 02" }}
     </span>
   </article>
   {{- end -}}
 </div>
 {{- end -}}
 {{- end -}}
\ No newline at end of file
diff --git a/admin/site/themes/afp/layouts/partials/header.html b/admin/site/themes/afp/layouts/partials/header.html
--- a/admin/site/themes/afp/layouts/partials/header.html
+++ b/admin/site/themes/afp/layouts/partials/header.html
@@ -1,38 +1,38 @@
 <header>
   {{ if and (ne .Kind "home") (ne .File.BaseFileName "search") -}}
   <form autocomplete="off" action="{{ "search" | absURL }}">
     <div class='form-container'>
-      <input id="searchInput" type="search" size="31" maxlength="255" value="" aria-label="Search the AFP" list="autocomplete"><button
-      id="searchButton" type="button"><img src="{{- .Site.BaseURL -}}images/search.svg" alt="Search" /></button>
+      <input id="search-input" type="search" size="31" maxlength="255" value="" aria-label="Search the AFP" list="autocomplete"><button
+      id="search-button" type="button"><img src="{{- .Site.BaseURL -}}images/search.svg" alt="Search" /></button>
       <datalist id="autocomplete">
       </datalist>
     </div>
   </form>
   {{ end -}}
   {{ .Scratch.Set "title" (default .Site.Title (default .Title .Params.name)) }}
   {{- if and (eq .Section "authors") (isset .Site.Data.authors (.Scratch.Get "title")) -}}
     {{- .Scratch.Set "title" (index (index .Site.Data.authors (.Scratch.Get "title")) "name") -}}
   {{- end -}}
-  <h1 {{ if or (eq .Kind "home" ) (eq .File.BaseFileName "search" ) -}}class="largeTopMargin" {{ end -}}>
+  <h1 {{ if or (eq .Kind "home" ) (eq .File.BaseFileName "search" ) -}}class="large-top-margin" {{ end -}}>
     {{ title (.Scratch.Get "title") | replaceRE "[A-Z]" "<span class='first'>$0</span>" | safeHTML -}}
     {{- if (eq .Section "dependencies") }} Dependents{{ end -}}
   </h1>
   <div>
     {{ if (eq .Section "authors") -}}
     {{ with (index $.Site.Data.authors .Title )}}
     {{ with .website}}
     <p><a href="{{ . }}">{{ . }}</a></p>
     {{- end -}}{{- end -}}{{- end -}}
     {{- $site := . -}}
     {{ with .Params.authors}}
     <p>{{- partial "authors.html" (dict "site" $site "authors" . "affiliations" $site.Params.affiliations) -}}
       {{ with $site.Params.contributors }}
       with contributions from {{ partial "authors.html" (dict "site" $site "authors" . "affiliations" $site.Params.affiliations) -}}
       {{ end }}
     </p>
     {{ end }}
     {{ with .Params.date }}
     <p class="date">{{- dateFormat "January 2, 2006" . -}}</p>
     {{ end }}
   </div>
 </header>
\ No newline at end of file
diff --git a/admin/site/themes/afp/layouts/partials/navigation.html b/admin/site/themes/afp/layouts/partials/navigation.html
--- a/admin/site/themes/afp/layouts/partials/navigation.html
+++ b/admin/site/themes/afp/layouts/partials/navigation.html
@@ -1,37 +1,37 @@
-<div id="menuToggle">
+<div id="menu-toggle">
   <input id="toggle" type="checkbox" />
   <label for="toggle">
     <span>menu</span>
     <img src="{{- .Site.BaseURL -}}images/menu.svg" alt="Menu" />
   </label>
 
-  <a href="{{- .Site.BaseURL -}}" class='logoLink'>
+  <a href="{{- .Site.BaseURL -}}" class='logo-link'>
     <img src="{{- .Site.BaseURL -}}images/afp.png" alt='Logo of the Archive of Formal Proofs' class="logo">
   </a>
 
   {{ if and (ne .Kind "home") (ne .File.TranslationBaseName "search") -}}
   <a href="/search"><img src="{{- .Site.BaseURL -}}images/search.svg" alt="Search" /></a>
   {{ end -}}
 
   <nav id="menu">
     <div>
-      <a href="{{- .Site.BaseURL -}}" class='logoLink'>
+      <a href="{{- .Site.BaseURL -}}" class='logo-link'>
         <img src="{{- .Site.BaseURL -}}images/afp.png" alt='Logo of the Archive of Formal Proofs' class="logo">
       </a>
       {{ $currentPage := . -}}
       <ul>
         {{- range .Site.Menus.main }}
         <li {{ if $currentPage.IsMenuCurrent "main" . }}class="active" {{ end }}><a href="{{- .URL -}}">{{- .Name -}}
           </a></li>
         {{- end }}
       </ul>
     </div>
     <ul>
       {{- range .Site.Menus.bottom }}
       <li {{ if $currentPage.IsMenuCurrent "bottom" . }}class="active" {{ end }}><a href="{{- .URL -}}">{{- .Name
           -}}</a>
       </li>
       {{- end }}
     </ul>
   </nav>
 </div>
\ No newline at end of file
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,32 @@
 {{- $entry_name := .File.BaseFileName -}}
 {{- $site := . -}}
 {{- $path := .Site.Params.afpUrls.html -}}
 {{- if isset .Site.Data "status" -}}
   {{- $path = .Site.Params.afpUrls.htmlDevel -}}
 {{- end -}}
-<div id="menuToggle">
-  <a href="{{- .Site.BaseURL -}}" class='logoLink'>
+<div id="menu-toggle">
+  <a href="{{- .Site.BaseURL -}}" class='logo-link'>
     <img src="{{- .Site.BaseURL -}}images/afp.png" alt='Logo of the Archive of Formal Proofs' class="logo">
   </a>
   <nav>
   <div>
     <a href="{{- .Site.BaseURL -}}">
       <img src="{{- .Site.BaseURL -}}images/afp.png" alt='Logo of the Archive of Formal Proofs'
         class="logo">
     </a>
     {{ $currentPage := . -}}
     <ul>
       <li><a href="{{- .Site.BaseURL -}}entries/{{- $entry_name | urlize -}}">Return to entry</a></li>
     </ul>
     <hr>
     <ul id="theory-navbar" class="list-group"></ul>
   </div>
   <ul>
     <li><a href="{{- $path -}}/{{- $entry_name -}}/outline.pdf">Proof
       outline</a></li>
     <li><a href="{{- $path -}}/{{- $entry_name -}}/document.pdf">Proof
       document</a></li>
     <li><a href="{{- $path -}}/{{- $entry_name -}}/session_graph.pdf">Session dependencies</a></li>
   </ul>
   </nav>
 </div>
diff --git a/admin/site/themes/afp/static/css/isabelle.css b/admin/site/themes/afp/static/css/isabelle.css
--- a/admin/site/themes/afp/static/css/isabelle.css
+++ b/admin/site/themes/afp/static/css/isabelle.css
@@ -1,137 +1,164 @@
 /* Isabelle fonts */
 
 @font-face {
   font-family: 'Isabelle DejaVu Sans Mono';
   src: url('/font/IsabelleDejaVuSansMono.ttf') format('truetype');
 }
 
 @font-face {
   font-family: 'Isabelle DejaVu Sans Mono';
   src: url('/font/IsabelleDejaVuSansMono-Bold.ttf') format('truetype');
   font-weight: bold;
 }
 
 /* standard document markup */
 
 dt {
   float: left;
   clear: left;
   padding-right: 0.5em;
   font-weight: bold;
 }
 
 body {
   color: #000000;
   background-color: #FFFFFF;
 }
 
 .head     { background-color: #FFFFFF; }
 .source   {
   direction: ltr; unicode-bidi: bidi-override;
   background-color: #FFFFFF;
   padding: 10px;
   font-family: "Isabelle DejaVu Sans Mono", monospace;
 }
 
 .theories { background-color: #FFFFFF; padding: 10px; }
 .sessions { background-color: #FFFFFF; padding: 10px; }
 .document { white-space: normal; font-family: "Isabelle DejaVu Serif", serif; }
 
 .name     { font-style: italic; }
 .filename { font-family: "Isabelle DejaVu Sans Mono", monospace; }
 
 
 /* basic syntax markup */
 
 .hidden         { font-family: Vacuous; font-size: 1%; color: rgba(255,255,255,0); }
 .control        { font-weight: bold; font-style: italic; }
 
 .binding        { color: #336655; }
 .tfree          { color: #A020F0; }
 .tvar           { color: #A020F0; }
 .free           { color: #0000FF; }
 .skolem         { color: #D2691E; }
 .bound          { color: #008000; }
 .var            { color: #00009B; }
 .numeral        { }
 .literal        { font-weight: bold; }
 .delimiter      { }
 .inner_numeral  { color: #FF0000; }
 .inner_quoted   { color: #FF00CC; }
 .inner_cartouche { color: #CC6600; }
 .comment1       { color: #CC0000; }
 .comment2       { color: #FF8400; }
 .comment3       { color: #6600CC; }
 .dynamic        { color: #7BA428; }
 .class_parameter_color { color: #D2691E; }
 
 .bold           { font-weight: bold; }
 
 .main           { color: #000000; }
 .command        { font-weight: bold; }
 .keyword        { font-weight: bold; }
 .keyword1       { color: #006699; }
 .keyword2       { color: #009966; }
 .keyword3       { color: #0099FF; }
 .quasi_keyword  { color: #9966FF; }
 .operator       { color: #323232; }
 .string         { color: #FF00CC; }
 .alt_string     { color: #CC00CC; }
 .verbatim       { color: #6600CC; }
 .cartouche      { color: #CC6600; }
 .comment        { color: #CC0000; }
 .improper       { color: #FF5050; }
 .antiquote      { color: #6600CC; }
 .raw_text       { color: #6600CC; }
 .plain_text     { color: #CC6600; }
 .bad            { background-color: #FF6A6A; }
 .quoted         { background-color: rgba(139,139,139,0.05); }
 .antiquoted     { background-color: rgba(255,200,50,0.1); }
 
 
 /* message background */
 
 .writeln_message      { background-color: #F0F0F0; }
 .information_message  { background-color: #DCEAF3; }
 .tracing_message      { background-color: #F0F8FF; }
 .warning_message      { background-color: #EEE8AA; }
 .legacy_message       { background-color: #EEE8AA; }
 .error_message        { background-color: #FFC1C1; }
 
 
 /* message underline */
 
 .writeln { border-bottom: 1px dotted #C0C0C0; }
 .information { border-bottom: 1px dotted #C1DFEE; }
 .warning { border-bottom: 1px dotted #FF8C00; }
 .legacy { border-bottom: 1px dotted #FF8C00; }
 .error { border-bottom: 1px dotted #B22222; }
 
 
 /* tooltips */
 
 .writeln { position: relative; display: inline-block; }
 .information { position: relative; display: inline-block; }
 .warning { position: relative; display: inline-block; }
 .legacy { position: relative; display: inline-block; }
 .error { position: relative; display: inline-block; }
 
 .writeln:hover .tooltip { visibility: visible; }
 .information:hover .tooltip { visibility: visible; }
 .warning:hover .tooltip { visibility: visible; }
 .legacy:hover .tooltip { visibility: visible; }
 .error:hover .tooltip { visibility: visible; }
 
 .tooltip {
   top: -0.5ex;
   left: 5em;
   visibility: hidden;
   width: 50em;
   border: 1px solid #808080;
   padding: 1px 1px;
   background-color: #FFFFE9;
   position: absolute;
   z-index: 1;
 }
 
 .tooltip pre { margin: 1px; white-space: pre-wrap; }
+
+
+/* formal entities */
+
+.entity_def {
+  color: inherit;
+  text-decoration: inherit;
+}
+
+.entity_def:hover {
+  color: inherit;
+  text-decoration: inherit;
+  background-color: rgba(50,50,50,20%);
+}
+
+.entity_ref {
+  color: inherit;
+  text-decoration: inherit;
+  border: 0.5px solid rgba(0,0,0,0);
+}
+
+.entity_ref:hover {
+  color: inherit;
+  text-decoration: inherit;
+  background-color: rgba(50,50,50,20%);
+  border: 0.5px solid black;
+}
diff --git a/admin/site/themes/afp/static/js/header-search.js b/admin/site/themes/afp/static/js/header-search.js
--- a/admin/site/themes/afp/static/js/header-search.js
+++ b/admin/site/themes/afp/static/js/header-search.js
@@ -1,60 +1,60 @@
 function load_search(input, keywords) {
   const suggest_index = get_suggest_index(keywords)
 
   input.addEventListener("keyup", function (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:
         if (this.value && this.value.length > 1) {
           add_suggestions(suggest_index, this.value)
         }
     }
   })
 
   input.addEventListener("keydown", function (event) {
     switch (event.key) {
       case "Enter":
         event.preventDefault() // prevent the form from being submitted
         handle_submit(this.value)
         break
       default:
     }
   })
 
   input.addEventListener("change", function () {
     handle_submit(this.value)
   })
 }
 
 function handle_submit(value) {
   if (typeof history.pushState !== "undefined") {
     document.location = window.location.origin + "/search/?s=" + value
   }
 }
 
 document.addEventListener("DOMContentLoaded", function () {
-  const input = document.getElementById("searchInput")
-  const button = document.getElementById("searchButton")
+  const input = document.getElementById("search-input")
+  const button = document.getElementById("search-button")
   if (button) {
     button.addEventListener("click", () => {
       handle_submit(input.value)
     })
   }
 
   Promise.all([fetch("/data/keywords.json")])
     .then(function (responses) {
       // Get a JSON object from each of the responses
       return Promise.all(responses.map((response) => response.json()))
     })
     .then((data) => load_search(input, ...data))
 })
diff --git a/admin/site/themes/afp/static/js/search.js b/admin/site/themes/afp/static/js/search.js
--- a/admin/site/themes/afp/static/js/search.js
+++ b/admin/site/themes/afp/static/js/search.js
@@ -1,302 +1,302 @@
 /* constants */
 
 const URL_FINDFACTS = 'https://search.isabelle.in.tum.de'
 
 const NUM_MAX_SIDE_RESULTS = 4
 const NUM_MAX_MAIN_RESULTS = 15
 
-const ID_SEARCH_INPUT = 'searchInput'
-const ID_SEARCH_BUTTON = 'searchButton'
+const ID_SEARCH_INPUT = 'search-input'
+const ID_SEARCH_BUTTON = 'search-button'
 const ID_RESULTS_ENTRIES = 'search-results'
 const ID_RESULTS_AUTHORS = 'author-results'
 const ID_RESULTS_TOPICS = 'topic-results'
 const ID_RESULTS_FINDFACTS = 'find-facts-results'
 
 
 /* index */
 
 function build_indexes(entries, authors, topics, keywords) {
   const entry_index = new FlexSearch.Document({
     encoder: 'advanced',
     tokenize: 'forward',
     document: {
       id: 'id',
       index: ['title', 'abstract', 'date', 'topics[]', 'authors[]'],
       store: true,
     },
   })
   entries.forEach(entry => entry_index.add(entry))
 
   const author_index = new FlexSearch.Document({
     encoder: 'advanced',
     tokenize: 'forward',
     document: {
       id: 'id',
       index: 'name',
       store: true
     },
   })
   authors.forEach(author => author_index.add(author))
 
   const topic_index = new FlexSearch.Document({
     encoder: 'icase',
     tokenize: 'forward',
     document: {
       id: 'id',
       index: 'name',
       store: true
     },
   })
   topics.forEach(topic => topic_index.add(topic))
 
   const suggest_index = get_suggest_index(keywords)
 
   return {
     entry: entry_index,
     author: author_index,
     topic: topic_index,
     suggest: suggest_index,
   }
 }
 
 async function get_findfacts_index() {
   const indexes = await fetch(URL_FINDFACTS + '/v1/indexes').then(async http_res => {
     if (http_res.status !== 200) {
       console.log(`Error ${http_res.status} when fetching indexes: ${http_res.statusText}`)
       return Promise.resolve([])
     }
     return await http_res.json()
   }).catch((err) => {
     console.log(`Could not fetch indexes: ${err}`)
     return Promise.resolve([])
   })
 
   return indexes.find(index => index.startsWith('default_'))
 }
 
 
 /* search */
 
 function local_search(indices, query) {
   const entry_results = [...new Set(indices['entry'].search(query, NUM_MAX_MAIN_RESULTS + 1,
     {enrich: true}).flatMap(e => e.result).map(d => d.doc))]
   const topic_results = indices['topic'].search(query, NUM_MAX_SIDE_RESULTS + 1,
     {enrich: true, pluck: 'name'}).map(d => d.doc)
   const author_results = indices['author'].search(query, NUM_MAX_SIDE_RESULTS + 1,
     {enrich: true, pluck: 'name'}).map(d => d.doc)
   return {entries: entry_results, topics: topic_results, authors: author_results}
 }
 
 async function findfacts_search(index, query) {
   if (!index) return {}
   const facet_query = {
     filters: [
       {
         field: 'SourceCode',
         filter: {
           Term: {
             inner: query
           }
         }
       }
     ],
     fields: ['Kind'],
     maxFacets: 5
   }
   const facet = await fetch(`${URL_FINDFACTS}/v1/${index}/facet`, {
       method: 'POST',
       mode: 'cors',
       headers: {
         'Content-Type': 'application/json',
       },
       body: JSON.stringify(facet_query),
     }
   ).then(async (response) => {
     if (response.status !== 200) {
       console.log(`Error ${http_res.status} on findfacts query: ${http_res.statusText}`)
       return {}
     } else {
       const json = await response.json()
       return json['Kind']
     }
   }).catch((err) => {
     console.log(`Error in findfacts query: ${err}`)
     return {}
   })
   const search_query = `{"term"%3A"${encodeURIComponent(query)}"}`
   const url = `${URL_FINDFACTS}/#search/${index}?q=${search_query}`
 
   return {facet: facet, url: url}
 }
 
 
 /* result handling */
 
 function render_entry(entry) {
   const authors = entry.authors.join(', ')
   const topics = entry.topics.map((topic, key) =>
     `<a href=/topics/${entry.topic_links[key]}>${topic}</a>`).join(', ')
   const year = entry.date.substring(0, 4)
 
   return `
   <div>
     <div class='title'>
       <h3>
         <a href='${entry.link}'>${entry.title}</a>
       </h3>
     </div>
     <div class='subtitle'>
       <span style="float:left">${authors}</span>
       <span style="float:right">${year}</span>
     </div>
     <div class='abstract mathjax_process'>${entry.abstract}</div>
     <div>in ${topics}</div>
   </div>`
 }
 
 function render_entries_results(data, query) {
   if (!data) return parse_elem('<p>Please enter a search term above.</p>')
   if (data.length === 0) return parse_elem('<p>No results.</p>')
   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('<p>No results</p>')
   else {
     const end = data.length > NUM_MAX_SIDE_RESULTS ? '<li>...</li>' : ''
     const res = parse_elem(`
       <ul>${data.slice(0, NUM_MAX_SIDE_RESULTS).map(item => `
         <li>
           <a href="${item.link}">${item.name}</a>
         </li>`).join('')}
         ${end}
       </ul>`)
     new Mark(res).mark(query)
     return res
   }
 }
 
 function render_findfacts_results(res) {
   if (res.facet && Object.keys(res.facet).length > 0) {
     return parse_elem(`
       <ul>${(Object.entries(res.facet).map(([name, count]) => `
         <li>
           <a href="${escape_html(res.url)}" target="_blank" rel="noreferrer noopener">
             ${count} ${name}s
           </a>
         </li>`).join(''))}
       </ul>`)
   } else return parse_elem('<p>No results</p>')
 }
 
 
 /* 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('<p>...</p>'))
       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)