Major website rewrite

Gemfile

@@ -5,4 +5,5 @@ gem "just-the-docs", "0.12.0"
 
 group :jekyll_plugins do
   gem 'jekyll-katex'
+  gem 'jekyll-redirect-from'
 end

Gemfile.lock

@@ -61,6 +61,8 @@ GEM
     jekyll-katex (1.0.0)
       execjs (~> 2.7)
       jekyll (>= 3.6, < 5.0)
+    jekyll-redirect-from (0.16.0)
+      jekyll (>= 3.3, < 5.0)
     jekyll-sass-converter (3.1.0)
       sass-embedded (~> 1.75)
     jekyll-seo-tag (2.8.0)
@@ -116,6 +118,7 @@ PLATFORMS
 DEPENDENCIES
   jekyll (~> 4.4)
   jekyll-katex
+  jekyll-redirect-from
   just-the-docs (= 0.12.0)
 
 BUNDLED WITH

_config.yml

@@ -9,6 +9,14 @@ aux_links:
 
 plugins:
   - jekyll-katex
+  - jekyll-redirect-from
+
+sass:
+  quiet_deps: true
+  silence_deprecations:
+    - color-functions
+    - global-builtin
+    - import
 
 callouts:
   highlight:

_data/linear_sequence.yml

@@ -0,0 +1,11 @@
+# Ordered reading sequence for the "Getting Started" linear path of the manual.
+# Only pages using `layout: linear` will show prev/next navigation, and they
+# must appear in this list for the links to resolve. Order here is the order
+# in which readers are expected to move through the pages.
+- manual/installation.md
+- manual/tutorial/index.md
+- manual/tutorial/hello-frog.md
+- manual/tutorial/otp-ots.md
+- manual/worked-examples/index.md
+- manual/worked-examples/chained-encryption.md
+- manual/worked-examples/kemdem-cpa.md

_includes/head_custom.html

@@ -1,3 +1,45 @@
 <link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/katex@0.11.1/dist/katex.min.css" integrity="sha384-zB1R0rpPzHqg7Kpt0Aljp8JPLqbXI3bhnPWROx27a9N0Ll6ZP/+DiW/UqRcLbRjq" crossorigin="anonymous">
-<script src="https://cdn.jsdelivr.net/npm/prismjs@1.29.0/prism.min.js"></script>
-<script src="{{ '/assets/js/prism-prooffrog.js' | relative_url }}"></script>
+
+<style>
+  img.lightbox { cursor: zoom-in; }
+  .lightbox-overlay {
+    position: fixed; inset: 0;
+    background: rgba(0, 0, 0, 0.85);
+    display: flex; align-items: center; justify-content: center;
+    z-index: 9999; cursor: zoom-out;
+    opacity: 0; transition: opacity 0.15s ease;
+  }
+  .lightbox-overlay.visible { opacity: 1; }
+  .lightbox-overlay img {
+    max-width: 95vw; max-height: 95vh;
+    box-shadow: 0 4px 32px rgba(0, 0, 0, 0.5);
+  }
+</style>
+
+<script>
+  document.addEventListener('DOMContentLoaded', function () {
+    var overlay = null;
+    function close() {
+      if (!overlay) return;
+      overlay.classList.remove('visible');
+      var o = overlay; overlay = null;
+      setTimeout(function () { if (o.parentNode) o.parentNode.removeChild(o); }, 150);
+      document.removeEventListener('keydown', onKey);
+    }
+    function onKey(e) { if (e.key === 'Escape') close(); }
+    document.querySelectorAll('img.lightbox').forEach(function (img) {
+      img.addEventListener('click', function () {
+        overlay = document.createElement('div');
+        overlay.className = 'lightbox-overlay';
+        var big = document.createElement('img');
+        big.src = img.currentSrc || img.src;
+        big.alt = img.alt;
+        overlay.appendChild(big);
+        overlay.addEventListener('click', close);
+        document.body.appendChild(overlay);
+        requestAnimationFrame(function () { overlay.classList.add('visible'); });
+        document.addEventListener('keydown', onKey);
+      });
+    });
+  });
+</script>

_includes/prev_next.html

@@ -0,0 +1,44 @@
+{%- comment -%}
+  Renders previous/next navigation for the linear reading path of the manual.
+  Used by _layouts/linear.html. Sequence is defined in _data/linear_sequence.yml.
+  Finds the current page by matching page.path against entries in the sequence,
+  then resolves neighbors to real page objects so we get URLs and titles for free.
+{%- endcomment -%}
+{%- assign seq = site.data.linear_sequence -%}
+{%- assign current_index = -1 -%}
+{%- for entry in seq -%}
+  {%- if entry == page.path -%}
+    {%- assign current_index = forloop.index0 -%}
+  {%- endif -%}
+{%- endfor -%}
+{%- if current_index >= 0 -%}
+  {%- assign prev_index = current_index | minus: 1 -%}
+  {%- assign next_index = current_index | plus: 1 -%}
+  {%- assign last_index = seq.size | minus: 1 -%}
+  {%- assign prev_path = "" -%}
+  {%- assign next_path = "" -%}
+  {%- for entry in seq -%}
+    {%- if forloop.index0 == prev_index -%}{%- assign prev_path = entry -%}{%- endif -%}
+    {%- if forloop.index0 == next_index -%}{%- assign next_path = entry -%}{%- endif -%}
+  {%- endfor -%}
+  {%- assign prev_page = site.pages | where: "path", prev_path | first -%}
+  {%- assign next_page = site.pages | where: "path", next_path | first -%}
+  <nav class="prev-next-nav" aria-label="Reading sequence navigation">
+    <div class="prev-next-nav__prev">
+      {%- if current_index > 0 and prev_page -%}
+        <a href="{{ prev_page.url | relative_url }}">
+          <span class="prev-next-nav__label">&larr; Previous</span>
+          <span class="prev-next-nav__title">{{ prev_page.title }}</span>
+        </a>
+      {%- endif -%}
+    </div>
+    <div class="prev-next-nav__next">
+      {%- if current_index < last_index and next_page -%}
+        <a href="{{ next_page.url | relative_url }}">
+          <span class="prev-next-nav__label">Next &rarr;</span>
+          <span class="prev-next-nav__title">{{ next_page.title }}</span>
+        </a>
+      {%- endif -%}
+    </div>
+  </nav>
+{%- endif -%}

_layouts/linear.html

@@ -0,0 +1,6 @@
+---
+layout: default
+---
+{{ content }}
+
+{% include prev_next.html %}

_plugins/rouge_prooffrog.rb

@@ -0,0 +1,65 @@
+# Rouge lexer for FrogLang (the ProofFrog language).
+#
+# Registers the `prooffrog` tag (plus per-file-type aliases) so that fenced
+# code blocks like ```prooffrog are syntax-highlighted server-side by Rouge
+# at Jekyll build time. This replaces the previous client-side Prism setup.
+#
+# The token set mirrors the old Prism grammar in assets/js/prism-prooffrog.js.
+
+require 'rouge'
+
+module Rouge
+  module Lexers
+    class ProofFrog < Rouge::RegexLexer
+      title 'ProofFrog'
+      desc 'FrogLang, the language of the ProofFrog proof assistant'
+      tag 'prooffrog'
+      aliases 'froglang', 'primitive', 'scheme', 'game', 'proof'
+      filenames '*.primitive', '*.scheme', '*.game', '*.proof'
+
+      # Top-level construct introducers
+      declarations = %w[Primitive Scheme Game Reduction Phase]
+
+      # Built-in types
+      builtins = %w[Bool Void Int BitString Set Map Array]
+
+      # Reserved words
+      keywords = %w[
+        import export as extends compose against requires
+        if else for return in to
+        union subsets induction from calls
+        Adversary oracles proof
+        let assume theorem games
+      ]
+
+      state :root do
+        rule %r(\s+), Text
+        rule %r(//.*), Comment::Single
+
+        # Single-quoted import path strings
+        rule %r('[^']*'), Str::Single
+
+        # Numbers: binary literals and decimal integers
+        rule %r(\b0b[01]+\b), Num::Bin
+        rule %r(\b\d+\b), Num::Integer
+
+        # None / true / false
+        rule %r(\bNone\b), Keyword::Constant
+        rule %r(\b(?:true|false)\b), Keyword::Constant
+
+        rule %r(\b(?:#{builtins.join('|')})\b), Name::Builtin
+        rule %r(\b(?:#{declarations.join('|')})\b), Keyword::Declaration
+        rule %r(\b(?:#{keywords.join('|')})\b), Keyword
+
+        # Operators (longest match first)
+        rule %r(<-|[=!<>]=|&&|\|\|), Operator
+        rule %r([+\-*/\\|!<>=]), Operator
+
+        rule %r([{}\[\]();:,.?]), Punctuation
+
+        rule %r(\w+), Name
+        rule %r(.), Text
+      end
+    end
+  end
+end

_sass/custom/custom.scss

@@ -9,7 +9,80 @@
 .token.number { color: #005cc5; }
 .token.operator { color: #d73a49; }
 .token.punctuation { color: #24292e; }
-pre:has(> code[class*="language-"]) { background: #f6f8fa; padding: 1em; }
+pre:has(> code[class*="language-"]) { background: $sidebar-color; padding: 1em; }
+
+// Code blocks: remove border, use sidebar background color
+div.highlighter-rouge,
+figure.highlight,
+.highlight,
+pre.highlight {
+  background-color: $sidebar-color;
+}
+
+div.highlighter-rouge div.highlight,
+figure.highlight pre,
+figure.highlight :not(pre) > code {
+  border: 0;
+  background-color: $sidebar-color;
+}
+
+.highlight .table-wrapper td,
+.highlight .table-wrapper pre {
+  background-color: $sidebar-color;
+}
+
+// Inline code: remove border, use sidebar background color
+:not(pre, figure) > code {
+  background-color: $sidebar-color;
+  border: 0;
+  padding-left: 3px;
+  padding-right: 3px;
+}
+
+// Prev/next navigation at the bottom of pages on the linear reading path.
+.prev-next-nav {
+  display: flex;
+  justify-content: space-between;
+  gap: 1rem;
+  margin-top: 3rem;
+  padding-top: 1.5rem;
+  border-top: 1px solid $border-color;
+
+  > div {
+    flex: 1 1 0;
+    min-width: 0;
+  }
+
+  &__next {
+    text-align: right;
+  }
+
+  a {
+    display: inline-block;
+    padding: 0.75rem 1rem;
+    border: 1px solid $border-color;
+    border-radius: 4px;
+    text-decoration: none;
+    max-width: 100%;
+
+    &:hover {
+      background-color: $sidebar-color;
+    }
+  }
+
+  &__label {
+    display: block;
+    font-size: 0.75rem;
+    text-transform: uppercase;
+    letter-spacing: 0.05em;
+    color: $grey-dk-000;
+  }
+
+  &__title {
+    display: block;
+    font-weight: 500;
+  }
+}
 
 .site-title::after {
 	background-image: url("../../prooffrog.png");
@@ -19,3 +92,12 @@ pre:has(> code[class*="language-"]) { background: #f6f8fa; padding: 1em; }
 	background-size: cover;
 	margin-left: 10px;
 }
+
+/* Label column: no left border, right-aligned */
+.table-labels td:last-child,
+.table-labels th:last-child {
+  border-left: none;
+  text-align: right;
+  width: 1%;
+  white-space: nowrap;
+}