diff --git a/admin/site/content/about.md b/admin/site/content/about.md
--- a/admin/site/content/about.md
+++ b/admin/site/content/about.md
@@ -1,54 +1,54 @@
 ---
 title: "About"
 menu: 
     main:
         name: "About"
         weight: 6
 ---
 
 The Archive of Formal Proofs is a collection of proof libraries, examples, and larger scientific developments,
 mechanically checked in the theorem prover Isabelle.
 It is organized in the way of a scientific journal.
 [Submissions](/submission) are refereed.
 
 The archive repository is hosted on [Heptapod](https://foss.heptapod.net/isa-afp/) to provide easy free access to archive entries.
 The entries are tested and maintained continuously against the current stable release of Isabelle.
 Older versions of archive entries will remain available.
 
 ## Editors
 
 The editors of the Archive of Formal Proofs are:
 
 *   [Manuel Eberl](http://www.in.tum.de/~eberlm/), [Technische Universität München](http://www.tum.de/)
 *   [Gerwin Klein](http://www.cse.unsw.edu.au/~kleing/), [Data61](http://www.data61.csiro.au)
 *   [Tobias Nipkow](http://www.in.tum.de/~nipkow/), [Technische Universität München](http://www.tum.de/)
 *   [Larry Paulson](http://www.cl.cam.ac.uk/users/lcp/), [University of Cambridge](http://www.cam.ac.uk/)
 *   [René Thiemann](http://cl-informatik.uibk.ac.at/users/thiemann/), [University of Innsbruck](https://www.uibk.ac.at/)
 
 ## Why
 
 We aim to strengthen the community and to foster the development of formal proofs.
 
 We hope that the Archive will provide:
 
 *   a resource of knowledge, examples, and libraries for users,
 *   a large and relevant test bed of theories for Isabelle developers, and
 *   a central, citable place for authors to publish their theories
 
 We encourage authors of publications that contain Isabelle developments to make their theories available in the Archive of Formal Proofs and to refer to the archive entry in their publication. It makes it easier for referees to check the validity of theorems (all entries in the Archive are mechanically checked), it makes it easier for readers of the publication to understand details of your development, and it makes it easier to use and build on your work.
 
 ## License
 
 All entries in the Archive of Formal Proofs are licensed under a [BSD-style License](LICENSE) or the [GNU LGPL](http://www.gnu.org/copyleft/lesser.html). This means they are free to download, free to use, free to change, and free to redistribute with minimal restrictions.
 
 The authors retain their full copyright on their original work, including their right to make the development available under another, additional license in the future.
 
 ## Website
 
 This website is the result of a project from the School of Informatics at the [University of Edinburgh](https://www.ed.ac.uk) by:
- * Carlin MacKenzie
- * James Vaughan, [AIML](https://aiml.inf.ed.ac.uk)
+ * Carlin MacKenzie, [AIML](https://aiml.inf.ed.ac.uk)
+ * James Vaughan, [AIAI](http://web.inf.ed.ac.uk/aiai/)
  * Jacques Fleuriot, [AIAI](http://web.inf.ed.ac.uk/aiai/)
 
 Integration and maintenance by:
  * [Fabian Huch](https://www21.in.tum.de/team/huch), [Technische Universität München](http://www.tum.de/)
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,1092 +1,1107 @@
 //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;
 }
 
 @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: 50vw;
+  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-break: break-all;
+    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);
   }
 
   .collapse-container.collapsed {
     .collapsible {
       display: none;
     }
     .invertible {
       transform: scale(1,-1);
     }
   }
 
   .content {
-    min-width: clamp(80ch,50vw, 50vw);
-    width: auto;
+    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: absolute;
-      right: 1em;
+      position: sticky;
+      right: 1rem;
+      float: right;
       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) {
+        @media screen and (min-width: $size-xl) {
             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) {
+  @media screen and (max-width: $size-s) {
     padding: 0;
     grid-template-columns: 1fr;
 
     .content {
       min-width: 350px;
       max-width: 100vw;
-      margin: 80px 0;
+      margin: 80px 0 0 20px;
+    }
+
+    h2 {
+      top: 60px;
     }
 
     nav {
       display: none;
     }
   }
 }
 
 .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);
   }
 
   form {
     display: none;
   }
 }
 
-@media (max-width: 650px) {
+@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-areas:
         'search'
         'sidebar'
         'entries';
     }
   }
 }
 
-@media (max-width: 875px) {
+@media screen and (max-width: $size-s) {
   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;
     }
   }
 
     
   .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-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 { 
       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;
 
     .logo-link {
       display: none;
     }
   }
 }
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,277 @@
 /* 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(`<body>${http_res.statusText}</body>`)
     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(`
       <div id="${to_collapsible_id(thy_name)}" class="${CLASS_COLLAPSIBLE}">
         <div id="${to_spinner_id(thy_name)}" class=${CLASS_LOADER}><div class=${CLASS_ANIMATION}></div></div>
       </div>`)
       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 = `<a id="${to_a_id(id)}" class="${CLASS_SPY_LINK}" href="#${id}">${escape_html(key)}</a>`
   } else {
     const head_id = to_id(thy_name, `${[...path, key, ...ref_parts[0]].join('.')}|${type}`)
     res = `<a id="${to_a_id(id)}" class="${CLASS_SPY_LINK}" href="#${head_id}">${escape_html(key)}</a>`
   }
 
   if (rec_ref.length > 1) {
     const by_key = group_by(rec_ref)
     const children = Object.keys(by_key).map((key1) => `
       <li>${nav_tree_rec(thy_name, [...path, key], key1, by_key[key1], type)}</li>`)
     return `
       ${res}
       <ul id="${to_ul_id(id)}" class="${CLASS_COLLAPSIBLE} ${CLASS_COLLAPSED}">
         ${children.join('')}
       </ul>`
   } else return res
 }
 
 function nav_tree(thy_name, refs, type) {
   let trees = Object.entries(group_by(refs || [])).map(([key, parts]) =>
     `<li>${nav_tree_rec(thy_name, [thy_name], key, parts, type)}</li>`)
 
   return parse_elem(`
     <ul id="${to_ul_id(thy_name)}" class="${CLASS_NAVBAR_TYPE} ${CLASS_COLLAPSIBLE} ${CLASS_COLLAPSED}">
       ${trees.join('')}
     </ul>`)
 }
 
 
 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(`<option value=${type}>${type}</option>`))
     }
 
     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(`
-        <div id="${to_container_id(thy_name)}" theory-src="${href}" class="${CLASS_COLLAPSE_CONTAINER} ${CLASS_COLLAPSED}">
+        <div id="${to_container_id(thy_name)}" theory-src="${href}" style="min-width: fit-content" class="${CLASS_COLLAPSE_CONTAINER} ${CLASS_COLLAPSED}">
           <h2 id="${to_id(thy_name)}" style="cursor: pointer" onclick="toggle_theory('${thy_name}')">
             ${thy_name}
           <svg id="${to_svg_id(thy_name)}" viewBox="0 0 10 10" aria-hidden="true" focusable="false"
                class="${CLASS_INVERTIBLE}">
             <path d="m1.6953 6.7407 3.3047-3.3929 3.3047 3.3927" fill="none" stroke-linecap="round"
                   stroke-linejoin="round" stroke-width="2"/>
           </svg>
           </h2>
         </div>`)
       theory.replaceWith(thy_collapsible)
     }
 
     const type = get_query(PARAM_NAVBAR_TYPE) ? get_query(PARAM_NAVBAR_TYPE) : NAVBAR_TYPES[0]
     navbar.appendChild(parse_elem(`
       <li>
         <select id=${ID_NAVBAR_TYPE_SELECTOR} onchange="change_selector(this.options[this.selectedIndex].value)">
           <option value=${type} selected="selected">${type}</option>
         </select>
       </li>`))
     navbar.append(...thy_names.map((thy_name) => parse_elem(`
       <li id="${to_nav_id(thy_name)}">
         <a id="${to_a_id(thy_name)}" class="${CLASS_SPY_LINK} ${CLASS_THY_NAV}" href="#${to_id(thy_name)}">
           ${thy_name}
         </a>
       </li>`)), parse_elem('<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)