Fix documentation for docs website

7 files changed, 695 insertions, 985 deletions

diff --git a/docs/.nojekyll b/docs/.nojekyll
new file mode 100644
index 0000000..e69de29
--- /dev/null
+++ b/docs/.nojekyll
diff --git a/docs/css/org.css b/docs/css/org.css
index aa713ec..99008e7 100644
--- a/docs/css/org.css
+++ b/docs/css/org.css
@@ -1,1058 +1,696 @@
-@media all
-{
-    body {
-        font-family: "Helvetica Neue", "Lucida Grande", "Lucida Sans Unicode", Helvetica, Arial, sans-serif !important;
-        font-size: 14px;
-        line-height: 21px;
-        color: #333;
+body {
+    width: 95%;
+    font-size: 14px;
+    margin: 2% auto;
+    line-height: 1.4em;
+    font-family: "Alegreya", serif;
+    color: #333;
+    background-color: #fdf6e3;
+}
 
-        max-width: 62em;
-        margin: auto;
-    }
-    body #content {
-        padding-top: 30px;
-    }
-    body .title {
-        margin-left: 0;
-    }
+#table-of-contents li, #toc li {
+    list-style-type: none;
+}
 
-    #org-div-home-and-up{
-        position: fixed;
-        right: 0;
-        top: 4em;
-    }
+.is-active-link::before {
+  background-color: #A5573E;
+}
 
-    /* TOC inspired by http://jashkenas.github.com/coffee-script */
-    #table-of-contents {
-        z-index: 100;
-        font-size: 10pt;
-        position: fixed;
-        right: 0em;
-        top: 0em;
-        background: white;
-        -webkit-box-shadow: 0 0 0.5em #777777;
-        -moz-box-shadow: 0 0 0.5em #777777;
-        -webkit-border-bottom-left-radius: 5px;
-        -moz-border-radius-bottomleft: 5px;
-        text-align: right;
-        /* ensure doesn't flow off the screen when expanded */
-        max-height: 80%;
-        overflow: auto; 
-    }
-    #table-of-contents h2 {
-        font-size: 10pt;
-        max-width: 9em;
-        font-weight: normal;
-        padding-left: 0.5em;
-        padding-left: 0.5em;
-        padding-top: 0.05em;
-        padding-bottom: 0.05em; 
+@media screen and (min-width: 600px) {
+    body {
+        font-size: 18px;
     }
+}
 
-    #table-of-contents #text-table-of-contents {
-        display: none;
-        text-align: left; 
-    }
-    #table-of-contents:hover #text-table-of-contents {
-        display: block;
-        padding: 0.5em;
-        margin-top: -1.5em; 
+@media screen and (min-width: 1200px) {
+    body {
+        margin: 2% 0;
+        margin-left: 27rem;
     }
 
-    #table-of-contents #text-table-of-contents ul {
-        list-style-position: outside;
+    #left-bar {
+        float: left;
+        position: fixed;
+        left: 0px;
+        top: 0px;
+        padding: 25px;
+        width: 20rem;
+        height: 100%;
+        background-color: #A5573E;
     }
 
-    /* #license { */
-    /*   padding: .3em; */
-    /*   border: 1px solid gray; */
-    /*   background-color: #eeeeee; */
-    /* } */
+    .logo > a {
+        color: #fdf6e3;
+        font-size: 5rem;
+        font-weight: bold;
+        text-decoration: none;
+    }
 
-    h1 {
-        /*
-          font-family:Sans;
-          font-weight:bold; */
-        font-size:2.1em;
-        padding:0 0 30px 0;
-        margin-top: 10px;
+    .logo {
+        text-align: center;
         margin-bottom: 10px;
-        color: #333;
     }
 
-    h2 {
-        font-family:Arial,sans-serif;
-        font-size:1.45em;
-        line-height:16px;
-        padding:7px 0 0 0;
-        color: #666;
+    .logo > a:hover {
+        border-bottom: none;
     }
 
-    .outline-text-2 {
-        margin-left: 0.1em
+    #navbar {
+        text-align: center;
     }
 
-    .title {
-
+    #navbar > span {
+        padding: 0 1em;
     }
 
-    h3 {
-        font-family:Arial,sans-serif;
-        font-size:1.3em;
-        color: #666;
-        margin-left: 0.6em;
+    #navbar > span > a {
+        color: #fdf6e3;
+        font-size: 1.5rem;
+        font-weight: bold;
     }
 
-    .outline-text-3 {
-        margin-left: 0.9em;
+    #navbar > span > a:hover {
+        border-bottom: none;
     }
 
-    h4 {
-        font-family:Arial,sans-serif;
-        font-size:1.2em;
-        margin-left: 1.2em;
-        color: #666;
+    a.toc-link {
+        color: #fdf6e3;
     }
 
-    .outline-text-4 {
-        margin-left: 1.45em;
+    header > p {
+        color: #fdf6e3;
+        line-height: 1.3;
     }
 
-    a {
-        text-decoration: none; 
-        color: #3399cc;
-    }
-    /* a:visited {text-decoration: none; color: #224444} */ /* Taken out because color too similar to text. */
-    a:visited {
-        text-decoration: none; 
-        color: #3399cc;
-    }  /* this is now the color of the Unicorns horn */
-    a:hover {
-        text-decoration: underline; 
-        color: #3399cc;
+    #postamble {
+        float: left;
+        position: fixed;
+        left: 50px;
+        bottom: 0;
+        max-width: 20rem;
     }
+}
 
-    ul, ol {
-        padding-left: 2em;
+@media screen and (min-width: 810px) {
+    body {
+        max-width: 800px;
     }
+}
 
-    ul {
-	list-style-type: square;
-	list-style-image: inherit;
-	list-style-position: outside;
-    }
-    ol {
-	list-style-type: decimal;
-	list-style-position: outside;
-    }
-    ol ol {
-	list-style-type: lower-alpha;
-    }
+::selection {
+    background: #D6EDFF;
+}
 
-    .todo {
-        color: #CA0000;
-    }
+p {
+    margin: 1em auto;
+}
 
-    .done {
-        color: #006666;
-    }
+ol,ul {
+    margin: 0 auto;
+}
 
-    .timestamp-kwd {
-        color: #444;
-    }
+dl {
+    margin: 0 auto;
+}
 
-    .tag {
+.title {
+    text-align: center;
+    margin: 0.8em auto;
+    color: black;
+}
 
-    }
+.subtitle {
+    text-align: center;
+    font-size: 0.7em;
+    line-height: 1.4;
+    font-weight: bold;
+    color: grey;
+    margin: 1em auto;
+}
 
-    li {
-        margin: .4em;
-    }
+.abstract {
+    margin: auto;
+    width: 80%;
+    font-style: italic;
+}
 
-    table {
-        border: none;
-        margin: auto;
-        margin-top: 10px;
-        margin-bottom: 10px;
-    }
+.abstract p:last-of-type:before {
+    content: "    ";
+    white-space: pre;
+}
 
-    td {
-        border: none;
-        border-left: 1px solid black;
-    }
+.status {
+    font-size: 90%;
+    margin: 2em auto;
+}
 
-    th {
-        border: none;
-    }
+[class^="section-number-"] {
+    margin-right: .5em;
+}
 
-    table.full {
-    }
+[id^="orgheadline"] {
+    clear: both;
+}
 
-    table.full td {
-	border: 1px solid black;
-	padding: 5px;
-    }
+#footnotes {
+    font-size: 90%;
+}
 
-    code {
-        font-size: 100%;
-        color: black;
-        border: 1px solid #DEDEDE;
-        padding: 0px 0.2em;
-    }
+.footpara {
+    display: inline;
+    margin: .2em auto;
+}
 
-    img {
-        border: none;
-    }
+.footdef {
+    margin-bottom: 1em;
+}
 
-    .share img {
-        opacity: .4;
-        -moz-opacity: .4;
-        filter: alpha(opacity=40);
-    }
+.footdef sup {
+    padding-right: .5em;
+}
 
-    .share img:hover {
-        opacity: 1;
-        -moz-opacity: 1;
-        filter: alpha(opacity=100);
-    }
+a {
+    color: #527d9a;
+    text-decoration: none;
+}
 
-    /* pre {border: 1px solid #555; */
-    /*      background: #EEE; */
-    /*      font-size: 9pt; */
-    /*      padding: 1em; */
-    /*     } */
-
-    /* pre { */
-    /*     color: #e5e5e5; */
-    /*     background-color: #000000; */
-    /*     padding: 1.4em; */
-    /*     border: 2px solid gray; */
-    /* } */
-
-    /* pre { */
-    /*     background-color: #2b2b2b; */
-    /*     border: 4px solid gray; */
-    /*     color: #EEE; */
-    /*     overflow: auto; */
-    /*     padding: 1em; */
-    /*  } */
-
-    pre {
-        font-family: Monaco, Consolas, "Lucida Console", monospace;
-        color: black;
-        background-color: #ffffff;
-        padding: 1.2em;
-        /* border: 1px solid #dddddd; */
-        overflow: auto;
-
-        /*
-        -webkit-box-shadow: 0px 0px 4px rgba(0,0,0,0.23);
-        -moz-box-shadow: 0px 0px 4px rgba(0,0,0,0.23);
-        box-shadow: 0px 0px 4px rgba(0,0,0,0.23);
-        */
-    }
+a:hover {
+    color: #003355;
+    border-bottom: 1px dotted;
+}
 
-    div.summary {
-        padding: 15px;
-        border:1px solid #CCC;
-        border-radius:10px;
-        -moz-border-radius:10px;
-        -webkit-box-shadow: 0px 0px 4px rgba(0,0,0,0.23);
-        -moz-box-shadow: 0px 0px 4px rgba(0,0,0,0.23);
-        box-shadow: 0px 0px 4px rgba(0,0,0,0.23);
-    }
+figure {
+    padding: 0px;
+    margin: 1em auto;
+    text-align: center;
+}
 
-    div.summary h2 {
-        padding: 0;
-        margin: 0;
-    }
+img {
+    max-width: 100%;
+    vertical-align: middle;
+}
 
-    .org-info-box {
-        clear:both;
-        margin-left:auto;
-        margin-right:auto;
-        padding:0.7em;
-    /* border:1px solid #CCC; */
-    /* border-radius:10px; */
-    /* -moz-border-radius:10px; */
-    }
-    .org-info-box img {
-        float:left;
-        margin:0em 0.5em 0em 0em;
-    }
-    .org-info-box p {
-        margin:0em;
-        padding:0em;
-    }
+.MathJax_Display {
+    margin: 0!important;
+    width: 90%!important;
+}
+
+h1,h2,h3,h4,h5,h6 {
+    color: #A5573E;
+    line-height: 1em;
+    font-family: "Iosevka", sans-serif;
+}
 
+h1,h2,h3 {
+    line-height: 1.4em;
+}
 
-    .builtin {
-        /* font-lock-builtin-face */
-        color: #f4a460;
-    }
-    .comment {
-        /* font-lock-comment-face */
-        color: #737373;
-    }
-    .comment-delimiter {
-        /* font-lock-comment-delimiter-face */
-        color: #666666;
-    }
-    .constant {
-        /* font-lock-constant-face */
-        color: #db7093;
-    }
-    .doc {
-        /* font-lock-doc-face */
-        color: #b3b3b3;
-    }
-    .function-name {
-        /* font-lock-function-name-face */
-        color: #5f9ea0;
-    }
-    .headline {
-        /* headline-face */
-        color: #ffffff;
-        background-color: #000000;
-        font-weight: bold;
-    }
-    .keyword {
-        /* font-lock-keyword-face */
-        color: #4682b4;
-    }
-    .negation-char {
-    }
-    .regexp-grouping-backslash {
-    }
-    .regexp-grouping-construct {
-    }
-    .string {
-        /* font-lock-string-face */
-        color: #ccc79a;
-    }
-    .todo-comment {
-        /* todo-comment-face */
-        color: #ffffff;
-        background-color: #000000;
-        font-weight: bold;
+h4,h5,h6 {
+    font-size: 1em;
+}
+
+@media screen and (min-width: 600px) {
+    h1 {
+        font-size: 2em;
     }
-    .variable-name {
-        /* font-lock-variable-name-face */
-        color: #ff6a6a;
+    h2 {
+        font-size: 1.5em;
     }
-    .warning {
-        /* font-lock-warning-face */
-        color: #ffffff;
-        background-color: #cd5c5c;
-        font-weight: bold;
+    h3 {
+        font-size: 1.3em;
     }
-    pre.a {
-        color: inherit;
-        background-color: inherit;
-        font: inherit;
-        text-decoration: inherit;
+    h1,h2,h3 {
+        line-height: 1.4em;
     }
-    pre.a:hover {
-        text-decoration: underline;
+    h4,h5,h6 {
+        font-size: 1.1em;
     }
+}
 
-    /* Styles for org-info.js */
+dt {
+    font-weight: bold;
+}
 
-    .org-info-js_info-navigation
-    {
-        border-style:none;
-    }
+/* table */
 
-    #org-info-js_console-label
-    {
-        font-size:10px;
-        font-weight:bold;
-        white-space:nowrap;
-    }
+table {
+    margin: 1em auto;
+    border-top: 2px solid;
+    border-bottom: 2px solid;
+    border-collapse: collapse;
+}
 
-    .org-info-js_search-highlight
-    {
-        background-color:#ffff00;
-        color:#000000;
-        font-weight:bold;
-    }
+thead {
+    border-bottom: 2px solid;
+}
 
-    #org-info-js-window
-    {
-        border-bottom:1px solid black;
-        padding-bottom:10px;
-        margin-bottom:10px;
-    }
+table td + td, table th + th {
+    border-left: 1px solid gray;
+}
 
+table tr {
+    border-top: 1px solid lightgray;
+}
 
+td,th {
+    padding: 0.3em 0.6em;
+    vertical-align: middle;
+}
 
-    .org-info-search-highlight
-    {
-        background-color:#adefef; /* same color as emacs default */
-        color:#000000;
-        font-weight:bold;
-    }
+caption.t-above {
+    caption-side: top;
+}
 
-    .org-bbdb-company {
-        /* bbdb-company */
-        font-style: italic;
-    }
-    .org-bbdb-field-name {
-    }
-    .org-bbdb-field-value {
-    }
-    .org-bbdb-name {
-        /* bbdb-name */
-        text-decoration: underline;
-    }
-    .org-bold {
-        /* bold */
-        font-weight: bold;
-    }
-    .org-bold-italic {
-        /* bold-italic */
-        font-weight: bold;
-        font-style: italic;
-    }
-    .org-border {
-        /* border */
-        background-color: #000000;
-    }
-    .org-buffer-menu-buffer {
-        /* buffer-menu-buffer */
-        font-weight: bold;
-    }
-    .org-builtin {
-        /* font-lock-builtin-face */
-        color: #da70d6;
-    }
-    .org-button {
-        /* button */
-        text-decoration: underline;
-    }
-    .org-c-nonbreakable-space {
-        /* c-nonbreakable-space-face */
-        background-color: #ff0000;
-        font-weight: bold;
-    }
-    .org-calendar-today {
-        /* calendar-today */
-        text-decoration: underline;
-    }
-    .org-comment {
-        /* font-lock-comment-face */
-        color: #b22222;
-    }
-    .org-comment-delimiter {
-        /* font-lock-comment-delimiter-face */
-        color: #b22222;
-    }
-    .org-constant {
-        /* font-lock-constant-face */
-        color: #5f9ea0;
-    }
-    .org-cursor {
-        /* cursor */
-        background-color: #000000;
-    }
-    .org-default {
-        /* default */
-        color: #000000;
-        background-color: #ffffff;
-    }
-    .org-diary {
-        /* diary */
-        color: #ff0000;
-    }
-    .org-doc {
-        /* font-lock-doc-face */
-        color: #bc8f8f;
-    }
-    .org-escape-glyph {
-        /* escape-glyph */
-        color: #a52a2a;
-    }
-    .org-file-name-shadow {
-        /* file-name-shadow */
-        color: #7f7f7f;
-    }
-    .org-fixed-pitch {
-    }
-    .org-fringe {
-        /* fringe */
-        background-color: #f2f2f2;
-    }
-    .org-function-name {
-        /* font-lock-function-name-face */
-        color: #0000ff;
-    }
-    .org-header-line {
-        /* header-line */
-        color: #333333;
-        background-color: #e5e5e5;
-    }
-    .org-help-argument-name {
-        /* help-argument-name */
-        font-style: italic;
-    }
-    .org-highlight {
-        /* highlight */
-        background-color: #b4eeb4;
-    }
-    .org-holiday {
-        /* holiday */
-        background-color: #ffc0cb;
-    }
-    .org-info-header-node {
-        /* info-header-node */
-        color: #a52a2a;
-        font-weight: bold;
-        font-style: italic;
-    }
-    .org-info-header-xref {
-        /* info-header-xref */
-        color: #0000ff;
-        text-decoration: underline;
-    }
-    .org-info-menu-header {
-        /* info-menu-header */
-        font-weight: bold;
-    }
-    .org-info-menu-star {
-        /* info-menu-star */
-        color: #ff0000;
-    }
-    .org-info-node {
-        /* info-node */
-        color: #a52a2a;
-        font-weight: bold;
-        font-style: italic;
-    }
-    .org-info-title-1 {
-        /* info-title-1 */
-        font-size: 172%;
-        font-weight: bold;
-    }
-    .org-info-title-2 {
-        /* info-title-2 */
-        font-size: 144%;
-        font-weight: bold;
-    }
-    .org-info-title-3 {
-        /* info-title-3 */
-        font-size: 120%;
-        font-weight: bold;
-    }
-    .org-info-title-4 {
-        /* info-title-4 */
-        font-weight: bold;
-    }
-    .org-info-xref {
-        /* info-xref */
-        color: #0000ff;
-        text-decoration: underline;
-    }
-    .org-isearch {
-        /* isearch */
-        color: #b0e2ff;
-        background-color: #cd00cd;
-    }
-    .org-italic {
-        /* italic */
-        font-style: italic;
-    }
-    .org-keyword {
-        /* font-lock-keyword-face */
-        color: #a020f0;
-    }
-    .org-lazy-highlight {
-        /* lazy-highlight */
-        background-color: #afeeee;
-    }
-    .org-link {
-        /* link */
-        color: #0000ff;
-        text-decoration: underline;
-    }
-    .org-link-visited {
-        /* link-visited */
-        color: #8b008b;
-        text-decoration: underline;
-    }
-    .org-match {
-        /* match */
-        background-color: #ffff00;
-    }
-    .org-menu {
-    }
-    .org-message-cited-text {
-        /* message-cited-text */
-        color: #ff0000;
-    }
-    .org-message-header-cc {
-        /* message-header-cc */
-        color: #191970;
-    }
-    .org-message-header-name {
-        /* message-header-name */
-        color: #6495ed;
-    }
-    .org-message-header-newsgroups {
-        /* message-header-newsgroups */
-        color: #00008b;
-        font-weight: bold;
-        font-style: italic;
-    }
-    .org-message-header-other {
-        /* message-header-other */
-        color: #4682b4;
-    }
-    .org-message-header-subject {
-        /* message-header-subject */
-        color: #000080;
-        font-weight: bold;
-    }
-    .org-message-header-to {
-        /* message-header-to */
-        color: #191970;
-        font-weight: bold;
-    }
-    .org-message-header-xheader {
-        /* message-header-xheader */
-        color: #0000ff;
-    }
-    .org-message-mml {
-        /* message-mml */
-        color: #228b22;
-    }
-    .org-message-separator {
-        /* message-separator */
-        color: #a52a2a;
-    }
-    .org-minibuffer-prompt {
-        /* minibuffer-prompt */
-        color: #0000cd;
-    }
-    .org-mm-uu-extract {
-        /* mm-uu-extract */
-        color: #006400;
-        background-color: #ffffe0;
-    }
-    .org-mode-line {
-        /* mode-line */
-        color: #000000;
-        background-color: #bfbfbf;
-    }
-    .org-mode-line-buffer-id {
-        /* mode-line-buffer-id */
-        font-weight: bold;
-    }
-    .org-mode-line-highlight {
-    }
-    .org-mode-line-inactive {
-        /* mode-line-inactive */
-        color: #333333;
-        background-color: #e5e5e5;
-    }
-    .org-mouse {
-        /* mouse */
-        background-color: #000000;
-    }
-    .org-negation-char {
-    }
-    .org-next-error {
-        /* next-error */
-        background-color: #eedc82;
-    }
-    .org-nobreak-space {
-        /* nobreak-space */
-        color: #a52a2a;
-        text-decoration: underline;
-    }
-    .org-org-agenda-date {
-        /* org-agenda-date */
-        color: #0000ff;
-    }
-    .org-org-agenda-date-weekend {
-        /* org-agenda-date-weekend */
-        color: #0000ff;
-        font-weight: bold;
-    }
-    .org-org-agenda-restriction-lock {
-        /* org-agenda-restriction-lock */
-        background-color: #ffff00;
-    }
-    .org-org-agenda-structure {
-        /* org-agenda-structure */
-        color: #0000ff;
-    }
-    .org-org-archived {
-        /* org-archived */
-        color: #7f7f7f;
-    }
-    .org-org-code {
-        /* org-code */
-        color: #7f7f7f;
-    }
-    .org-org-column {
-        /* org-column */
-        background-color: #e5e5e5;
-    }
-    .org-org-column-title {
-        /* org-column-title */
-        background-color: #e5e5e5;
-        font-weight: bold;
-        text-decoration: underline;
-    }
-    .org-org-date {
-        /* org-date */
-        color: #a020f0;
-        text-decoration: underline;
-    }
-    .org-org-done {
-        /* org-done */
-        color: #228b22;
-        font-weight: bold;
-    }
-    .org-org-drawer {
-        /* org-drawer */
-        color: #0000ff;
-    }
-    .org-org-ellipsis {
-        /* org-ellipsis */
-        color: #b8860b;
-        text-decoration: underline;
-    }
-    .org-org-formula {
-        /* org-formula */
-        color: #b22222;
-    }
-    .org-org-headline-done {
-        /* org-headline-done */
-        color: #bc8f8f;
-    }
-    .org-org-hide {
-        /* org-hide */
-        color: #e5e5e5;
-    }
-    .org-org-latex-and-export-specials {
-        /* org-latex-and-export-specials */
-        color: #8b4513;
-    }
-    .org-org-level-1 {
-        /* org-level-1 */
-        color: #0000ff;
-    }
-    .org-org-level-2 {
-        /* org-level-2 */
-        color: #b8860b;
-    }
-    .org-org-level-3 {
-        /* org-level-3 */
-        color: #a020f0;
-    }
-    .org-org-level-4 {
-        /* org-level-4 */
-        color: #b22222;
-    }
-    .org-org-level-5 {
-        /* org-level-5 */
-        color: #228b22;
-    }
-    .org-org-level-6 {
-        /* org-level-6 */
-        color: #5f9ea0;
-    }
-    .org-org-level-7 {
-        /* org-level-7 */
-        color: #da70d6;
-    }
-    .org-org-level-8 {
-        /* org-level-8 */
-        color: #bc8f8f;
-    }
-    .org-org-link {
-        /* org-link */
-        color: #a020f0;
-        text-decoration: underline;
-    }
-    .org-org-property-value {
-    }
-    .org-org-scheduled-previously {
-        /* org-scheduled-previously */
-        color: #b22222;
-    }
-    .org-org-scheduled-today {
-        /* org-scheduled-today */
-        color: #006400;
-    }
-    .org-org-sexp-date {
-        /* org-sexp-date */
-        color: #a020f0;
-    }
-    .org-org-special-keyword {
-        /* org-special-keyword */
-        color: #bc8f8f;
-    }
-    .org-org-table {
-        /* org-table */
-        color: #0000ff;
-    }
-    .org-org-tag {
-        /* org-tag */
-        font-weight: bold;
-    }
-    .org-org-target {
-        /* org-target */
-        text-decoration: underline;
-    }
-    .org-org-time-grid {
-        /* org-time-grid */
-        color: #b8860b;
-    }
-    .org-org-todo {
-        /* org-todo */
-        color: #ff0000;
-    }
-    .org-org-upcoming-deadline {
-        /* org-upcoming-deadline */
-        color: #b22222;
-    }
-    .org-org-verbatim {
-        /* org-verbatim */
-        color: #7f7f7f;
-        text-decoration: underline;
-    }
-    .org-org-warning {
-        /* org-warning */
-        color: #ff0000;
-        font-weight: bold;
-    }
-    .org-outline-1 {
-        /* outline-1 */
-        color: #0000ff;
-    }
-    .org-outline-2 {
-        /* outline-2 */
-        color: #b8860b;
-    }
-    .org-outline-3 {
-        /* outline-3 */
-        color: #a020f0;
-    }
-    .org-outline-4 {
-        /* outline-4 */
-        color: #b22222;
-    }
-    .org-outline-5 {
-        /* outline-5 */
-        color: #228b22;
-    }
-    .org-outline-6 {
-        /* outline-6 */
-        color: #5f9ea0;
-    }
-    .org-outline-7 {
-        /* outline-7 */
-        color: #da70d6;
-    }
-    .org-outline-8 {
-        /* outline-8 */
-        color: #bc8f8f;
-    }
-    .outline-text-1, .outline-text-2, .outline-text-3, .outline-text-4, .outline-text-5, .outline-text-6 {
-    /* Add more spacing between section. Padding, so that folding with org-info.js works as expected. */
+caption.t-bottom {
+    caption-side: bottom;
+}
 
-    }
+caption {
+    margin-bottom: 0.3em;
+}
 
-    .org-preprocessor {
-        /* font-lock-preprocessor-face */
-        color: #da70d6;
-    }
-    .org-query-replace {
-        /* query-replace */
-        color: #b0e2ff;
-        background-color: #cd00cd;
-    }
-    .org-regexp-grouping-backslash {
-        /* font-lock-regexp-grouping-backslash */
-        font-weight: bold;
-    }
-    .org-regexp-grouping-construct {
-        /* font-lock-regexp-grouping-construct */
-        font-weight: bold;
-    }
-    .org-region {
-        /* region */
-        background-color: #eedc82;
-    }
-    .org-rmail-highlight {
-    }
-    .org-scroll-bar {
-        /* scroll-bar */
-        background-color: #bfbfbf;
-    }
-    .org-secondary-selection {
-        /* secondary-selection */
-        background-color: #ffff00;
-    }
-    .org-shadow {
-        /* shadow */
-        color: #7f7f7f;
-    }
-    .org-show-paren-match {
-        /* show-paren-match */
-        background-color: #40e0d0;
-    }
-    .org-show-paren-mismatch {
-        /* show-paren-mismatch */
-        color: #ffffff;
-        background-color: #a020f0;
-    }
-    .org-string {
-        /* font-lock-string-face */
-        color: #bc8f8f;
-    }
-    .org-texinfo-heading {
-        /* texinfo-heading */
-        color: #0000ff;
-    }
-    .org-tool-bar {
-        /* tool-bar */
-        color: #000000;
-        background-color: #bfbfbf;
-    }
-    .org-tooltip {
-        /* tooltip */
-        color: #000000;
-        background-color: #ffffe0;
-    }
-    .org-trailing-whitespace {
-        /* trailing-whitespace */
-        background-color: #ff0000;
-    }
-    .org-type {
-        /* font-lock-type-face */
-        color: #228b22;
-    }
-    .org-underline {
-        /* underline */
-        text-decoration: underline;
-    }
-    .org-variable-name {
-        /* font-lock-variable-name-face */
-        color: #b8860b;
-    }
-    .org-variable-pitch {
-    }
-    .org-vertical-border {
-    }
-    .org-warning {
-        /* font-lock-warning-face */
-        color: #ff0000;
-        font-weight: bold;
-    }
-    .rss_box {
-    }
-    .rss_title, rss_title a {
-    }
-    .rss_items {
-    }
-    .rss_item a:link, .rss_item a:visited, .rss_item a:active {
-    }
-    .rss_item a:hover {
-    }
-    .rss_date {
-    }
+figcaption {
+    margin-top: 0.3em;
+}
 
-    #postamble {
-        padding: .3em;
-        margin-bottom: 1em;
-        border: 1px solid gray;
-        background-color: #eeeeee;
-    }
+th.org-right {
+    text-align: center;
+}
 
-    #show_source {
-        float: right; 
-        margin: .7em;
-    }
-    
+th.org-left {
+    text-align: center;
+}
+
+th.org-center {
+    text-align: center;
+}
+
+td.org-right {
+    text-align: right;
+}
 
-} /* END OF @media all */
+td.org-left {
+    text-align: left;
+}
 
+td.org-center {
+    text-align: center;
+}
 
+blockquote {
+    margin: 1em 2em;
+    padding-left: 1em;
+    border-left: 3px solid #ccc;
+}
 
-@media screen
-{
-  #table-of-contents {
-    float: right;
-    padding-right: 5px;
-    border: 1px solid #CCC;
-    max-width: 50%;
-    overflow: auto;
-  }
-} /* END OF @media screen */
+kbd {
+    background-color: #f7f7f7;
+    font-size: 80%;
+    margin: 0 .1em;
+    padding: .1em .6em;
+}
+
+.todo {
+    background-color: red;
+    color: white;
+    padding: .1em 0.3em;
+    border-radius: 3px;
+    background-clip: padding-box;
+    font-size: 80%;
+    font-family: "Iosevka", monospace;
+    line-height: 1;
+}
 
-.due {
+.done {
+    background-color: green;
+    color: white;
+    padding: .1em 0.3em;
+    border-radius: 3px;
+    background-clip: padding-box;
     font-size: 80%;
-    margin: 0 1em 0 1em;
+    font-family: "Iosevka", monospace;
+    line-height: 1;
+}
+
+.priority {
+    color: orange;
+    font-family: "Iosevka", monospace;
+}
+
+/* Because tag span is set to float.  This is more like a hacking.  Maybe we
+   need a cleaner solution. */
+#table-of-contents li {
+    clear: both;
+}
+
+.tag {
+    font-family: "Iosevka", monospace;
+    font-size: 0.7em;
+    font-weight: normal;
+}
+
+.tag span {
+    padding: 0.3em 0.3em;
+    float: right;
+    margin-right: .5em;
+    border: 1px solid #bbb;
+    border-radius: 3px;
+    background-clip: padding-box;
+    color: #333;
+    background-color: #eee;
+    line-height: 1;
+}
+
+.timestamp {
+    color: #bebebe;
+    font-size: 90%;
 }
 
-#contact-front p {
+.timestamp-kwd {
+    color: #5f9ea0;
+}
+
+.org-right {
+    margin-left: auto;
+    margin-right: 0px;
+    text-align: right;
+}
+
+.org-left {
+    margin-left: 0px;
+    margin-right: auto;
     text-align: left;
 }
 
-ul.index-links {
-    padding-left: 0;
-    margin-left: 0;
+.org-center {
+    margin-left: auto;
+    margin-right: auto;
+    text-align: center;
 }
 
-ul.index-links li {
-    list-style-type: none;
-    margin-left: 0;
+.underline {
+    text-decoration: underline;
+}
+
+#postamble p, #preamble p {
+    font-size: 90%;
+    margin: .2em;
+}
+
+p.verse {
+    margin-left: 3%;
 }
 
-div#preamble div#plupperButton a img {
-    height: 16px;
+:not(pre) > code {
+    padding: 2px 5px;
+    margin: auto 1px;
+    border: 1px solid #DDD;
+    border-radius: 3px;
+    background-clip: padding-box;
+    color: #333;
+    font-size: 80%;
+}
+
+.org-src-container {
+    border: 1px solid #ccc;
+    box-shadow: 3px 3px 3px #eee;
+    font-family: "Iosevka", monospace;
+    font-size: 80%;
+    margin: 1em auto;
+    padding: 0.1em 0.5em;
+    position: relative;
+}
+
+.org-src-container>pre {
+    overflow: auto;
+}
+
+.org-src-container>pre:before {
+    display: block;
     position: absolute;
-    top: 4px;
+    background-color: #b3b3b3;
+    top: 0;
+    right: 0;
+    padding: 0 0.5em;
+    border-bottom-left-radius: 8px;
+    border: 0;
+    color: white;
+    font-size: 80%;
 }
 
-blockquote {
-    background: #fbfbfb;
+/* from http://demo.thi.ng/org-spec/ */
+
+.org-src-container>pre.src-sh:before {
+    content: 'sh';
+}
+.org-src-container>pre.src-bash:before {
+    content: 'bash';
+}
+.org-src-container>pre.src-emacs-lisp:before {
+    content: 'Emacs Lisp';
+}
+.org-src-container>pre.src-R:before {
+    content: 'R';
+}
+.org-src-container>pre.src-org:before {
+    content: 'Org';
+}
+.org-src-container>pre.src-cpp:before {
+    content: 'C++';
+}
+.org-src-container>pre.src-c:before {
+    content: 'C';
+}
+.org-src-container>pre.src-html:before {
+    content: 'HTML'
+}
+.org-src-container>pre.src-js:before {
+    content: 'Javascript'
+}
+.org-src-container>pre.src-javascript:before {
+    content: 'Javascript'
+}
+
+// More languages from http://orgmode.org/worg/org-contrib/babel/languages.html
+
+.org-src-container>pre.src-abc:before {
+    content: 'ABC';
+}
+.org-src-container>pre.src-asymptote:before {
+    content: 'Asymptote';
+}
+.org-src-container>pre.src-awk:before {
+    content: 'Awk';
+}
+.org-src-container>pre.src-C:before {
+    content: 'C';
+}
+.org-src-container>pre.src-calc:before {
+    content: 'Calc';
+}
+.org-src-container>pre.src-clojure:before {
+    content: 'Clojure';
+}
+.org-src-container>pre.src-comint:before {
+    content: 'comint';
+}
+.org-src-container>pre.src-css:before {
+    content: 'CSS';
+}
+.org-src-container>pre.src-D:before {
+    content: 'D';
+}
+.org-src-container>pre.src-ditaa:before {
+    content: 'Ditaa';
+}
+.org-src-container>pre.src-dot:before {
+    content: 'Dot';
+}
+.org-src-container>pre.src-ebnf:before {
+    content: 'ebnf';
+}
+.org-src-container>pre.src-forth:before {
+    content: 'Forth';
+}
+.org-src-container>pre.src-F90:before {
+    content: 'Fortran';
+}
+.org-src-container>pre.src-gnuplot:before {
+    content: 'Gnuplot';
+}
+.org-src-container>pre.src-haskell:before {
+    content: 'Haskell';
+}
+.org-src-container>pre.src-io:before {
+    content: 'Io';
+}
+.org-src-container>pre.src-java:before {
+    content: 'Java';
+}
+.org-src-container>pre.src-latex:before {
+    content: 'LaTeX';
+}
+.org-src-container>pre.src-ledger:before {
+    content: 'Ledger';
+}
+.org-src-container>pre.src-ly:before {
+    content: 'Lilypond';
+}
+.org-src-container>pre.src-lisp:before {
+    content: 'Lisp';
+}
+.org-src-container>pre.src-makefile:before {
+    content: 'Make';
+}
+.org-src-container>pre.src-matlab:before {
+    content: 'Matlab';
+}
+.org-src-container>pre.src-max:before {
+    content: 'Maxima';
+}
+.org-src-container>pre.src-mscgen:before {
+    content: 'Mscgen';
+}
+.org-src-container>pre.src-Caml:before {
+    content: 'Objective';
+}
+.org-src-container>pre.src-octave:before {
+    content: 'Octave';
+}
+.org-src-container>pre.src-org:before {
+    content: 'Org';
+}
+.org-src-container>pre.src-perl:before {
+    content: 'Perl';
+}
+.org-src-container>pre.src-picolisp:before {
+    content: 'Picolisp';
+}
+.org-src-container>pre.src-plantuml:before {
+    content: 'PlantUML';
+}
+.org-src-container>pre.src-python:before {
+    content: 'Python';
+}
+.org-src-container>pre.src-ruby:before {
+    content: 'Ruby';
+}
+.org-src-container>pre.src-sass:before {
+    content: 'Sass';
+}
+.org-src-container>pre.src-scala:before {
+    content: 'Scala';
+}
+.org-src-container>pre.src-scheme:before {
+    content: 'Scheme';
+}
+.org-src-container>pre.src-screen:before {
+    content: 'Screen';
+}
+.org-src-container>pre.src-sed:before {
+    content: 'Sed';
+}
+.org-src-container>pre.src-shell:before {
+    content: 'shell';
+}
+.org-src-container>pre.src-shen:before {
+    content: 'Shen';
+}
+.org-src-container>pre.src-sql:before {
+    content: 'SQL';
+}
+.org-src-container>pre.src-sqlite:before {
+    content: 'SQLite';
+}
+.org-src-container>pre.src-stan:before {
+    content: 'Stan';
+}
+.org-src-container>pre.src-vala:before {
+    content: 'Vala';
+}
+.org-src-container>pre.src-axiom:before {
+    content: 'Axiom';
+}
+.org-src-container>pre.src-browser:before {
+    content: 'HTML';
+}
+.org-src-container>pre.src-cypher:before {
+    content: 'Neo4j';
+}
+.org-src-container>pre.src-elixir:before {
+    content: 'Elixir';
+}
+.org-src-container>pre.src-request:before {
+    content: 'http';
+}
+.org-src-container>pre.src-ipython:before {
+    content: 'iPython';
+}
+.org-src-container>pre.src-kotlin:before {
+    content: 'Kotlin';
+}
+.org-src-container>pre.src-Flavored Erlang  lfe:before {
+    content: 'Lisp';
+}
+.org-src-container>pre.src-mongo:before {
+    content: 'MongoDB';
+}
+.org-src-container>pre.src-prolog:before {
+    content: 'Prolog';
+}
+.org-src-container>pre.src-rec:before {
+    content: 'rec';
+}
+.org-src-container>pre.src-ML  sml:before {
+    content: 'Standard';
+}
+.org-src-container>pre.src-Translate  translate:before {
+    content: 'Google';
+}
+.org-src-container>pre.src-typescript:before {
+    content: 'Typescript';
+}
+.org-src-container>pre.src-rust:before {
+    content: 'Rust';
+}
+
+.inlinetask {
+    background: #ffffcc;
+    border: 2px solid gray;
+    margin: 10px;
     padding: 10px;
-    border-radius: 10px;
-    -moz-border-radius: 10px;
 }
 
-.figure img {
-    background: white;
-    padding: 5px;
-    -moz-box-shadow: 0px 0px 5px #c7c7c7;
-    -webkit-box-shadow: 0px 0px 5px #c7c7c7;
-    box-shadow: 0px 0px 5px #c7c7c7;
+#org-div-home-and-up {
+    font-size: 70%;
+    text-align: right;
+    white-space: nowrap;
 }
 
-div.hidden > strong {
-    margin-left: 0;
-    cursor: pointer;
-    color: #aaa;
+.linenr {
+    font-size: 90%;
 }
 
-div.hidden > strong > small {
-    margin-left: 1em;
+.code-highlighted {
+    background-color: #ffff00;
+}
+
+#bibliography {
     font-size: 90%;
-    font-weight: normal;
-    font-style: italic;
 }
 
-div.hidden div.hidden-content {
-    padding-left: 10px;
-    margin-bottom: 4em;
-    border-left: 3px solid #999;
+#bibliography table {
+    width: 100%;
 }
 
-div.hidden {
-    margin-bottom: 1em;
-    margin-left: 2em;
+.creator {
+    display: block;
+
+}
+
+@media screen and (min-width: 600px) {
+    .creator {
+        display: inline;
+        float: right;
+    }
 }
diff --git a/docs/building.org b/docs/documentation.org
index 48a6a90..09c3ffe 100644
--- a/docs/building.org
+++ b/docs/documentation.org
@@ -1,5 +1,7 @@
-#+SETUPFILE: setup.org
-#+TITLE: Building
+#+SETUPFILE: publish.setup
+#+TITLE: Vericert Documentation
+
+* Building
 
 To build Vericert, the provided Makefile can be used. External dependencies are needed to build the project, which can be pulled in automatically with [[https://nixos.org/nix/][nix]] using the provided ~default.nix~ and ~shell.nix~ files.
 
@@ -15,7 +17,7 @@ The project is written in Coq, a theorem prover, which is extracted to OCaml so
 
 These dependencies can be installed manually, or automatically through Nix.
 
-* Downloading CompCert
+** Downloading CompCert
 
 CompCert is added as a submodule in the ~lib/CompCert~ directory. It is needed to run the build process below, as it is the one dependency that is not downloaded by nix, and has to be downloaded together with the repository. To clone CompCert together with this project, you can run:
 
@@ -29,7 +31,7 @@ If the repository is already cloned, you can run the following command to make s
 git submodule update --init
 #+end_src
 
-* Setting up Nix
+** Setting up Nix
 
 Nix is a package manager that can create an isolated environment so that the builds are reproducible. Once nix is installed, it can be used in the following way.
 
@@ -41,7 +43,7 @@ nix-shell
 
 which will open a shell that has all the dependencies loaded.
 
-* Makefile build
+** Makefile build
 
 If the dependencies were installed manually, or if one is in the ~nix-shell~, the project can be built by running:
 
@@ -57,7 +59,7 @@ make install
 
 Which will install the binary in ~./bin/vericert~ by default. However, this can be changed by changing the ~PREFIX~ environment variable, in which case the binary will be installed in ~$PREFIX/bin/vericert~.
 
-* Running
+** Running
 
 To test out ~vericert~ you can try the following examples which are in the test folder using the following:
 
diff --git a/docs/index.org b/docs/index.org
index 6ec0130..7a92650 100644
--- a/docs/index.org
+++ b/docs/index.org
@@ -1,5 +1,5 @@
-#+SETUPFILE: setup.org
-#+TITLE: VeriCert
+#+SETUPFILE: publish.setup
+#+TITLE: Vericert
 
 A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [[https://github.com/AbsInt/CompCert][CompCert]].  This ensures the correctness of the C to Verilog translation according to our Verilog semantics and CompCert's C semantics, removing the need to check the resulting hardware for behavioural correctness.
 
@@ -14,5 +14,5 @@ The project is currently a work in progress, so proofs remain to be finished.  C
 
 * Content
 
-- [[./docs/toc.html][Vericert Coq Documentation]]
-- [[./building.org][Building Vericert]]
+- [[./proof/toc.html][Vericert Proof]]
+- [[./documentation.org][Vericert Documentation]]
diff --git a/docs/publish.el b/docs/publish.el
index e7a27d7..df7235d 100644
--- a/docs/publish.el
+++ b/docs/publish.el
@@ -1,14 +1,89 @@
 ;; Publishing projects, this one is for the zettelkasten
+(require 'package)
+(package-initialize)
+(add-to-list 'package-archives '("org" . "https://orgmode.org/elpa/") t)
+(add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t)
+(package-refresh-contents)
+(package-install 'org-plus-contrib)
+(package-install 'htmlize)
+
 (require 'org)
+(require 'ox-publish)
+
+(defvar vericert/header "")
+(defvar vericert/site-attachments nil)
+(defvar vericert/base "")
+
+(setq vericert/base "/vericert")
+
+(setq vericert/header (concat "<div id=\"left-bar\">
+<header id=\"header\" class=\"status\">
+<div class=\"logo\"><a href=\"" vericert/base "\">Vericert</a></div>
+<nav id=\"navbar\">
+<span><a href=\"" vericert/base "/documentation.html\">Documentation</a></span>
+<span><a href=\"" vericert/base "/proof/toc.html\">Proof</a></span>
+</nav>
+<p>Vericert is the first formally verified high-level synthesis tool.</p>
+</header>
+<div id=\"toc\"></div>
+</div>"))
+
+(setq vericert/site-attachments
+  (regexp-opt '("jpg" "jpeg" "gif" "png" "svg"
+                "ico" "cur" "css" "js" "woff" "html" "pdf")))
+
+(setq user-full-name nil)
+
+(setq org-export-with-smart-quotes t
+      org-export-with-section-numbers t
+      org-export-with-toc t)
+
+(setq org-html-divs '((preamble "header" "header")
+                      (content "main" "content")
+                      (postamble "footer" "postamble"))
+      org-html-container-element "section"
+      org-html-metadata-timestamp-format "%Y-%m-%d"
+      org-html-checkbox-type 'html
+      org-html-html5-fancy t
+      org-html-validation-link nil
+      org-html-doctype "html5"
+      org-html-coding-system 'utf-8-unix
+      org-html-head-include-default-style nil
+      org-html-head-include-scripts nil)
+
 (setq org-publish-project-alist
-      '(("orgfiles"
-         :base-directory "./"
-         :base-extension "org"
-         :publishing-directory "./html/"
-         :publishing-function org-html-publish-to-html)
-        ("assets"
-         :base-directory "./css/"
-         :base-extension "css"
-         :publishing-directory "./html/css/"
-         :publishing-function org-publish-attachment)
-        ("documentation" :components ("orgfiles" "assets"))))
+      (list
+       (list "vericert-org"
+             :base-directory "./"
+             :base-extension "org"
+             :exclude (regexp-opt '("README" "draft"))
+             :html-head-extra
+             (concat "<script src=\"https://cdnjs.cloudflare.com/ajax/libs/tocbot/4.11.1/tocbot.min.js\"></script>
+<link rel=\"stylesheet\" href=\"https://cdnjs.cloudflare.com/ajax/libs/tocbot/4.11.1/tocbot.css\">
+<link rel=\"stylesheet\" href=\"" vericert/base "/css/org.css\" type=\"text/css\" media=\"screen\" />")
+             :html-preamble t
+             :html-preamble-format (list (list "en" vericert/header))
+             :html-postamble t
+             :html-postamble-format '(("en" "<script>tocbot.init({
+  tocSelector: '#toc',
+  contentSelector: '#content',
+  headingSelector: 'h2, h3',
+  hasInnerContainers: true,
+});</script>"))
+             :publishing-directory "./html"
+             :publishing-function 'org-html-publish-to-html
+             :recursive t)
+       (list "vericert-assets"
+             :base-directory "."
+             :base-extension vericert/site-attachments
+             :include '(".nojekyll")
+             :exclude "html/"
+             :publishing-directory "./html"
+             :publishing-function 'org-publish-attachment
+             :recursive t)
+       (list "vericert" :components '("vericert-org" "vericert-assets"))))
+
+(defun publish-vericert-docs ()
+  "Publish Vericert documentation."
+  (interactive)
+  (org-publish "vericert" t))
diff --git a/docs/publish.setup b/docs/publish.setup
new file mode 100644
index 0000000..a3e7255
--- /dev/null
+++ b/docs/publish.setup
@@ -0,0 +1,2 @@
+#+MACRO: begin-summary #+HTML: <div class="summary"><h2>Summary</h2>
+#+MACRO: end-summary #+HTML: </div>
diff --git a/docs/setup.org b/docs/setup.org
deleted file mode 100644
index 969fdf9..0000000
--- a/docs/setup.org
+++ /dev/null
@@ -1,7 +0,0 @@
-#+HTML_HEAD: <link rel="stylesheet" href="css/org.css" type="text/css" media="screen" />
-
-#+MACRO: begin-summary #+HTML: <div class="summary"><h2>Summary</h2>
-#+MACRO: end-summary #+HTML: </div>
-
-#+MACRO: begin-hidden #+HTML: <div class="hidden"><strong>$1 <small>click to toggle</small></strong><div class="hidden-content">
-#+MACRO: end-hidden #+HTML: </div></div>