diff --git a/_includes/head_custom.html b/_includes/head_custom.html
index a79c82e..a34fec3 100644
--- a/_includes/head_custom.html
+++ b/_includes/head_custom.html
@@ -2,3 +2,4 @@
 <link rel="preconnect" href="https://fonts.gstatic.com" crossorigin>
 <link href="https://fonts.googleapis.com/css2?family=Atkinson+Hyperlegible:wght@400;700&family=JetBrains+Mono:wght@400;600&display=swap" rel="stylesheet">
 <link rel="sitemap" type="application/xml" title="Sitemap" href="{{ '/sitemap.xml' | absolute_url }}">
+<script src="{{ '/assets/js/appearance.js' | relative_url }}"></script>
diff --git a/_includes/header_custom.html b/_includes/header_custom.html
new file mode 100644
index 0000000..ce05ad9
--- /dev/null
+++ b/_includes/header_custom.html
@@ -0,0 +1,11 @@
+<div class="appearance-control">
+  <button id="appearance" type="button" aria-label="Switch to dark mode" title="Switch to dark mode">
+    <svg class="appearance-moon" viewBox="0 0 24 24" aria-hidden="true" fill="none" stroke="currentColor" stroke-width="1.75" stroke-linecap="round" stroke-linejoin="round">
+      <path d="M20.5 13.2A8.5 8.5 0 0 1 10.8 3.5a8.5 8.5 0 1 0 9.7 9.7Z" />
+    </svg>
+    <svg class="appearance-sun" viewBox="0 0 24 24" aria-hidden="true" fill="none" stroke="currentColor" stroke-width="1.75" stroke-linecap="round">
+      <circle cx="12" cy="12" r="4" />
+      <path d="M12 2v2m0 16v2M2 12h2m16 0h2M4.9 4.9l1.4 1.4m11.4 11.4 1.4 1.4m0-14.2-1.4 1.4M6.3 17.7l-1.4 1.4" />
+    </svg>
+  </button>
+</div>
diff --git a/_includes/nav_footer_custom.html b/_includes/nav_footer_custom.html
index 155ab07..5793a8a 100644
--- a/_includes/nav_footer_custom.html
+++ b/_includes/nav_footer_custom.html
@@ -1,4 +1,4 @@
-<footer class="site-footer">
+<footer class="site-footer d-none d-md-block">
   Help improve this documentation by contributing on
   <a href="https://github.com/liquid-java/liquidjava-docs">GitHub</a>
 </footer>
diff --git a/_layouts/default.html b/_layouts/default.html
index 8ee9fe0..5eff81a 100644
--- a/_layouts/default.html
+++ b/_layouts/default.html
@@ -20,7 +20,7 @@
     {% include components/header.html %}
     <div class="main-content-wrap">
       {% include components/breadcrumbs.html %}
-      <div id="main-content" class="main-content">
+      <div id="main-content" class="main-content" tabindex="-1">
         <main>
           {% if site.heading_anchors != false %}
             {% include vendor/anchor_headings.html html=content beforeHeading="true" anchorBody="<svg viewBox=\"0 0 16 16\" aria-hidden=\"true\"><use xlink:href=\"#svg-link\"></use></svg>" anchorClass="anchor-heading" anchorAttrs="aria-labelledby=\"%html_id%\"" %}
diff --git a/_sass/custom/appearance.scss b/_sass/custom/appearance.scss
new file mode 100644
index 0000000..5aedb21
--- /dev/null
+++ b/_sass/custom/appearance.scss
@@ -0,0 +1,154 @@
+.search-input::placeholder, .search-icon { color: #66707b; }
+
+.appearance-control {
+  display: none;
+  align-items: center;
+  padding: .5rem 1rem;
+  flex-shrink: 0;
+  font-size: .75rem;
+
+  button {
+    display: grid;
+    place-items: center;
+    width: 2.5rem;
+    height: 2.5rem;
+    padding: .5rem;
+    border: 0;
+    border-radius: .5rem;
+    background: transparent;
+    color: #2a2f36;
+    font: inherit;
+    cursor: pointer;
+  }
+}
+
+:root[data-theme] .appearance-control { display: flex; }
+.appearance-control button:hover { background: #e5e9ed; }
+.appearance-control svg { width: 1.25rem; height: 1.25rem; }
+.appearance-sun { display: none; }
+:root[data-theme="dark"] .appearance-moon { display: none; }
+:root[data-theme="dark"] .appearance-sun { display: block; }
+
+.appearance-control button:focus-visible {
+  outline: 2px solid #5f7ea1;
+  outline-offset: 3px;
+}
+
+// keep appearance available when the mobile navigation is collapsed
+@media (max-width: 49.99rem) {
+  body .side-bar + .main .main-header,
+  body .side-bar + .main .main-header.nav-open { display: flex; }
+  .search { min-width: 0; }
+  .appearance-control { padding-left: 0; }
+}
+
+@mixin dark-appearance {
+  color-scheme: dark;
+
+  body { color: #c9d2de; background: #141a23; }
+  h1, h2, h3, h4, h5, h6, #toctitle { color: #edf2f8; }
+  a, .main-content a { color: #9cc9ec; }
+  a:not([class]) { text-decoration-color: #526b82; }
+  a:not([class]):hover { text-decoration-color: #9cc9ec; }
+  :focus-visible { outline-color: #9cc9ec; }
+  hr { background: #303c4c; }
+
+  .side-bar {
+    background: radial-gradient(ellipse at top left, rgba(104, 151, 194, .08), transparent 65%), #191f29;
+    border-color: #303c4c;
+  }
+  .site-header, .main-header, .site-nav, .site-footer { border-color: #303c4c; }
+  body .side-bar + .main .main-header { background: #141a23; }
+  .site-title { color: #edf2f8 !important; }
+  .site-title:hover, .site-button:hover { background: #242f3e; }
+  .site-footer { color: #9baabc; }
+  .icon, .site-button, .nav-list .nav-list-item .nav-list-expander { color: #9cc9ec; }
+  .nav-list .nav-list-item > .nav-list .nav-list-item .nav-list-link,
+  .nav-list .nav-list-item > .nav-list .nav-list-item .nav-list-expander { color: #b8c7d8; }
+  .nav-list .nav-list-item .nav-list-link:hover,
+  .nav-list .nav-list-item .nav-list-link.active,
+  .nav-list .nav-list-item .nav-list-expander:hover {
+    background: linear-gradient(90deg, rgba(104, 151, 194, .04), rgba(104, 151, 194, .16));
+    color: #d1e9ff;
+  }
+  .nav-list-link.active { box-shadow: inset 3px 0 #8dbce2; }
+  .breadcrumb-nav-list-item::after { color: #77889b; }
+
+  .search-input, .search-results, .search-result { color: #c9d2de; background: #191f29; }
+  .search-input { background: #141a23; }
+  .search-input::placeholder, .search-icon { color: #9baabc; }
+  .search-result:hover, .search-result.active { background: #243244; }
+  .search-result-title, .search-result-doc, .search-result-section { color: #d1e9ff; }
+  .search-result-preview { color: #b8c7d8; }
+  .search-result-previews { border-color: #405169; }
+  .search-result-doc.search-result-doc-parent { opacity: 1; color: #9baabc; }
+  .search-result-doc .search-result-icon { color: #9baabc; }
+  .search-result-rel-url { color: #9baabc; }
+  .search-result-highlight { color: #edf2f8; }
+  .search-results { border: 1px solid #303c4c; box-shadow: 0 16px 40px #0006; }
+
+  .appearance-control { color: #9baabc; }
+  .appearance-control button { color: #dce6f2; }
+  .appearance-control button:hover { background: #29394c; }
+  .appearance-control button:focus-visible { outline-color: #9cc9ec; }
+
+  .main-content :not(pre) > code { color: #d1e9ff; background: #253142; border-color: #35465b; }
+  .main-content pre.highlight,
+  .main-content div.highlighter-rouge,
+  .main-content #lj-editor,
+  .main-content .lj-output {
+    background: #101620;
+    border-color: #344256;
+    box-shadow: none;
+  }
+  .main-content .highlight .c,
+  .main-content .highlight .cm,
+  .main-content .highlight .c1,
+  .main-content .highlight .cs { color: #9baabc; }
+  .main-content img:not(.home-banner img) { border-color: #344256; box-shadow: none; }
+  .home-banner img { filter: brightness(.82) saturate(.9); }
+  .home-banner { border: 1px solid #344256; background: #101620; }
+  .main-content blockquote { background: #1d2836; border-color: #718da9; }
+
+  .card-panel, .page-nav-link {
+    background: #1c2531;
+    border-color: #334154;
+    box-shadow: none;
+  }
+  .card-panel:hover, .page-nav-link:hover { background: #232f3e; border-color: #6383a2; box-shadow: none; }
+  .page-nav-label { color: #9baabc; }
+  .page-nav-title { color: #dce6f2; }
+  .page-nav-link:focus-visible { outline: 2px solid #9cc9ec; outline-offset: 3px; box-shadow: none; }
+  .main-content .home-button { background: #9cc9ec; color: #142332; box-shadow: none; }
+  .main-content .home-button:hover { background: #bcdef7; color: #142332; }
+  th, td { background: #1c2531; border-color: #334154; }
+  thead th { background: #253142; border-color: #405169; color: #edf2f8; }
+  .table-wrapper { border: 1px solid #334154; box-shadow: none; }
+
+  @each $name, $accent, $surface in (note, #9cc9ec, #1d2c3d), (tip, #a7d9b9, #1d302d), (warn, #e5c784, #322e23) {
+    .main-content p.#{$name}, .main-content blockquote.#{$name} {
+      background: $surface;
+      border-color: $accent;
+      box-shadow: none;
+      &::before, > .#{$name}-title { color: $accent; }
+    }
+  }
+
+  .lj-toolbar label { color: #b8c7d8; }
+  .lj-toolbar select { color: #dce6f2; background: #202b39; border-color: #405169; }
+  .lj-toolbar select:hover { background: #29394c; border-color: #8dbce2; }
+  .lj-toolbar button { color: #9cc9ec; border-color: #405169; }
+  .lj-toolbar button:hover:not(:disabled) { background: #29394c; border-color: #8dbce2; }
+  .lj-toolbar #lj-verify, .lj-toolbar #lj-reset { color: #142332; background: #9cc9ec; border-color: #9cc9ec; }
+  .lj-toolbar #lj-verify:hover:not(:disabled), .lj-toolbar #lj-reset:hover { color: #142332; background: #bcdef7; border-color: #bcdef7; }
+  .lj-toolbar #lj-verify[data-state="busy"] { color: #fff; background: #a8323d; border-color: #cb6871; }
+  .lj-toolbar #lj-verify[data-state="busy"]:hover { background: #bd3d49; }
+  .lj-toolbar button:disabled, .lj-toolbar #lj-verify:disabled { color: #9baabc; background: #293342; border-color: #405169; }
+}
+
+:root[data-theme="dark"] { @include dark-appearance; }
+
+// the system theme also works without JavaScript
+@media (prefers-color-scheme: dark) {
+  :root:not([data-theme]) { @include dark-appearance; }
+}
diff --git a/_sass/custom/custom.scss b/_sass/custom/custom.scss
index 24b58e6..7ae2af1 100644
--- a/_sass/custom/custom.scss
+++ b/_sass/custom/custom.scss
@@ -1,5 +1,10 @@
-.site-header {
-  border-bottom: 1px solid rgba(23, 26, 31, 0.08);
+.site-header,
+.main-header {
+  border-bottom: 0;
+}
+
+.main-content > hr {
+  display: none;
 }
 
 .site-title {
@@ -30,6 +35,7 @@
 
 .site-footer {
   color: $body-text-color;
+  text-align: left;
 }
 
 .main-content a {
@@ -247,6 +253,14 @@
   list-style: disc;
 }
 
+.main-content ul > li::before {
+  content: none;
+}
+
+.main-content .task-list-item {
+  list-style: none;
+}
+
 .main-content li > ul,
 .main-content li > ol {
   margin-top: 0.35rem;
@@ -332,7 +346,6 @@
   gap: 0.75rem;
   margin: 2.25rem 0 0.25rem;
   padding-top: 1.25rem;
-  border-top: 1px solid rgba(17, 24, 39, 0.08);
 }
 
 .page-nav-link {
@@ -401,3 +414,5 @@
     grid-template-columns: repeat(2, minmax(0, 1fr));
   }
 }
+
+@import "custom/appearance";
diff --git a/assets/js/appearance.js b/assets/js/appearance.js
new file mode 100644
index 0000000..696fecd
--- /dev/null
+++ b/assets/js/appearance.js
@@ -0,0 +1,35 @@
+(() => {
+  const root = document.documentElement;
+  const system = window.matchMedia('(prefers-color-scheme: dark)');
+  const key = 'liquidjava-appearance';
+  let preference = 'system';
+  let button;
+  try {
+    const saved = localStorage.getItem(key);
+    if (['light', 'dark'].includes(saved)) preference = saved;
+  } catch (_) { /* appearance still works when storage is unavailable */ }
+
+  function apply() {
+    root.dataset.theme = preference === 'system'
+      ? (system.matches ? 'dark' : 'light') : preference;
+    if (button) {
+      const label = root.dataset.theme === 'dark' ? 'Switch to light mode' : 'Switch to dark mode';
+      button.setAttribute('aria-label', label);
+      button.title = label;
+    }
+  }
+  apply();
+  system.addEventListener('change', apply);
+
+  document.addEventListener('DOMContentLoaded', () => {
+    button = document.getElementById('appearance');
+    apply();
+    button.addEventListener('click', () => {
+      preference = root.dataset.theme === 'dark' ? 'light' : 'dark';
+      try {
+        localStorage.setItem(key, preference);
+      } catch (_) { /* keep the selection for this page */ }
+      apply();
+    });
+  });
+})();
diff --git a/pages/command-line-interface.md b/pages/command-line-interface.md
index 3abbd8c..c26954d 100644
--- a/pages/command-line-interface.md
+++ b/pages/command-line-interface.md
@@ -1,6 +1,6 @@
 ---
 title: Command-Line Interface
-nav_order: 5
+nav_order: 6
 permalink: /command-line-interface/
 description: Run the LiquidJava verifier from the command line for local checks, debugging, and CI workflows.
 ---
diff --git a/pages/diagnostics/errors.md b/pages/diagnostics/errors.md
index d3e7e4c..e38300e 100644
--- a/pages/diagnostics/errors.md
+++ b/pages/diagnostics/errors.md
@@ -14,6 +14,7 @@ An error can be caused by a refinement violation, an invalid refinement, or anot
 | --- | --- |
 | `RefinementError` | A refinement was violated or could not be proven |
 | `StateRefinementError` | A state refinement was violated or could not be proven |
+| `SMTUnknownError` | The solver could not determine whether a refinement holds |
 | `NotFoundError` | An element used in a refinement could not be found |
 | `SyntaxError` | The syntax used in a refinement is invalid |
 | `ArgumentMismatchError` | A ghost or state invocation has the wrong number or type of arguments |
diff --git a/pages/diagnostics/index.md b/pages/diagnostics/index.md
index 49da1e2..4b456e3 100644
--- a/pages/diagnostics/index.md
+++ b/pages/diagnostics/index.md
@@ -1,6 +1,6 @@
 ---
 title: Diagnostics
-nav_order: 3
+nav_order: 4
 has_children: true
 has_toc: false
 permalink: /diagnostics/
diff --git a/pages/examples/index.md b/pages/examples/index.md
index 00c0de5..92d2991 100644
--- a/pages/examples/index.md
+++ b/pages/examples/index.md
@@ -1,6 +1,6 @@
 ---
 title: Examples
-nav_order: 6
+nav_order: 7
 has_children: true
 permalink: /examples/
 description: LiquidJava example usages with focused code snippets.
diff --git a/pages/resources.md b/pages/resources.md
index 0571b12..9d2a206 100644
--- a/pages/resources.md
+++ b/pages/resources.md
@@ -1,6 +1,6 @@
 ---
 title: Resources
-nav_order: 7
+nav_order: 8
 has_children: false
 permalink: /resources/
 description: Find LiquidJava papers, posters, and source repositories for deeper reading and experimentation.
@@ -14,7 +14,7 @@ description: Find LiquidJava papers, posters, and source repositories for deeper
 
 ## Posters
 
-- [Usability-Oriented Design of Liquid Types for Java](https://icse2023.paperlessevents.com.au/share/Gamboa-85), ICSE 2023 Digital Poster Session
+- [Usability-Oriented Design of Liquid Types for Java](https://conf.researchr.org/details/icse-2023/icse-2023-technical-track/142/Usability-Oriented-Design-of-Liquid-Types-for-Java), ICSE 2023 Poster Session
 - [LiquidJava: Adding Lightweight Verification to Java](https://catarinagamboa.github.io/assets/docs/poster_LiquidJava.pdf), INForum 2021
 - [Improving the Usability of LiquidJava](https://rcosta358.github.io/improving_the_usability_of_liquidjava.pdf), 11th LASIGE Workshop Poster Session
 - [Barista: Synthesizing Typestate Specifications with LLM Agents](https://rcosta358.github.io/barista.pdf), 11th LASIGE Workshop Poster Session
diff --git a/pages/verification/conditionals.md b/pages/verification/conditionals.md
new file mode 100644
index 0000000..d6f2341
--- /dev/null
+++ b/pages/verification/conditionals.md
@@ -0,0 +1,53 @@
+---
+title: Conditionals
+parent: Verification Features
+nav_order: 2
+permalink: /verification/conditionals/
+description: Learn how if and else conditions provide facts for refinement checks.
+---
+
+# Conditionals
+
+An `if` condition adds information along each branch. The `then` branch is checked assuming the condition is true; the `else` branch is checked assuming it is false.
+
+```java
+import liquidjava.specification.Refinement;
+
+public class ConditionalExample {
+    public static void requirePositive(
+            @Refinement("_ > 0") int value) {}
+    public static void requireNonPositive(
+            @Refinement("_ <= 0") int value) {}
+
+    public static void guarded(int value) {
+        if (value > 0) {
+            requirePositive(value); // accepted: value > 0
+        } else {
+            requireNonPositive(value); // accepted: value <= 0
+        }
+    }
+}
+```
+
+Although `guarded` accepts any integer, each call is protected by a condition that establishes the required refinement. No extra refinement on its parameter is needed for these calls.
+
+## The Condition Must Be Strong Enough
+
+Changing the guard to `value >= 0` does not prove strict positivity, because zero remains possible:
+
+```java
+import liquidjava.specification.Refinement;
+
+public class WeakGuardExample {
+    public static void requirePositive(
+            @Refinement("_ > 0") int value) {}
+
+    public static void guarded(int value) {
+        if (value >= 0) {
+            requirePositive(value); // Refinement Error: value could be 0
+        }
+    }
+}
+```
+
+Branch assumptions apply to the paths on which they hold. After an `if`/`else` where both branches continue, code must work for either outcome; it cannot assume that the `then` condition is still true. Nested conditions can provide additional facts inside their branches.
diff --git a/pages/verification/index.md b/pages/verification/index.md
new file mode 100644
index 0000000..093d561
--- /dev/null
+++ b/pages/verification/index.md
@@ -0,0 +1,36 @@
+---
+title: Verification Features
+nav_order: 3
+has_children: true
+has_toc: false
+permalink: /verification/
+description: Understand how LiquidJava checks assignments, method calls, conditionals, and recursive methods.
+---
+
+# Verification Features
+
+The [Annotations]({{ '/annotations/' | relative_url }}) section explains how to write specifications. This section explains how LiquidJava uses them when checking Java code, without running the program.
+
+At a check, the verifier gathers facts about the values in scope and asks an SMT solver whether those facts imply the required refinement. For example, knowing `x == 5` is enough to prove `x > 0`. Knowing only `x >= 0` is not: `x` could be zero.
+
+## Variables and Assignments
+
+A local variable's initializer must satisfy its declared refinement. Later assignments must satisfy that same refinement, even when the value changes.
+
+```java
+import liquidjava.specification.Refinement;
+
+public class AssignmentExample {
+    public static void example() {
+        @Refinement("_ > 0") int count = 1;
+        count = 2; // accepted: 2 > 0
+        count = 0; // Refinement Error: 0 is not positive
+    }
+}
+```
+
+The verifier also tracks information from expressions and assignments. An unannotated local such as `int count = 1` can therefore carry useful information; it does not declare a requirement that every later value must equal `1`.
+
+## When a Check Fails
+
+A refinement error means the verifier could not establish the required predicate from the available facts. The code may violate the requirement, or the verifier may need a stronger parameter refinement, a branch condition, or a return contract to establish it. See [Understanding Refinement Errors]({{ '/diagnostics/understanding-refinement-errors/' | relative_url }}) for interpreting the diagnostic and its counterexample.
diff --git a/pages/verification/method-calls.md b/pages/verification/method-calls.md
new file mode 100644
index 0000000..dcbcd37
--- /dev/null
+++ b/pages/verification/method-calls.md
@@ -0,0 +1,54 @@
+---
+title: Method Calls and Returns
+parent: Verification Features
+nav_order: 1
+permalink: /verification/method-calls/
+description: Learn how parameter and return refinements connect a method's implementation to its callers.
+---
+
+# Method Calls and Returns
+
+A method contract has two sides:
+
+- **Parameters:** callers must establish each parameter's refinement. The method body can assume those refinements.
+- **Return value:** each return must satisfy the method's declared refinement. Callers can use that refinement for the result.
+
+```java
+import liquidjava.specification.Refinement;
+
+public class MethodExample {
+    @Refinement("_ == value")
+    public static int positiveIdentity(
+            @Refinement("value > 0") int value) {
+        return value;
+    }
+
+    public static void example() {
+        @Refinement("_ == 3") int result = positiveIdentity(3);
+        positiveIdentity(0); // Refinement Error: 0 is not positive
+    }
+}
+```
+
+For `positiveIdentity(3)`, the verifier checks `3 > 0`. It then substitutes the argument into the return contract `_ == value`, so the result is known to equal `3`. The call with `0` fails the parameter check.
+
+The body is checked separately using its parameter contract. Returning a value that contradicts its return contract also produces an error:
+
+```java
+import liquidjava.specification.Refinement;
+
+public class ReturnExample {
+    @Refinement("_ > 0")
+    public static int positive() {
+        return 0; // Refinement Error: 0 is not positive
+    }
+}
+```
+
+Write the return properties callers need explicitly. For example, without a return refinement on `positiveIdentity`, callers should not rely on the verifier inspecting its body to discover that the result equals the argument.
+
+## Object State at a Call
+
+For a method with [state refinements]({{ '/annotations/state-refinement/' | relative_url }}), the verifier also checks that the receiver satisfies `from` before the call and uses `to` to describe its state afterward. A constructor's `to` establishes the initial state. This is how a protocol can reject a `read()` call after `close()`.
+
+For library methods whose source is outside the checked code, use [external refinements]({{ '/annotations/external-refinements-for/' | relative_url }}) to supply contracts. Those contracts describe the library behavior the verifier relies on; they do not verify the library's implementation.
diff --git a/pages/verification/recursion.md b/pages/verification/recursion.md
new file mode 100644
index 0000000..5de994d
--- /dev/null
+++ b/pages/verification/recursion.md
@@ -0,0 +1,57 @@
+---
+title: Recursion
+parent: Verification Features
+nav_order: 3
+permalink: /verification/recursion/
+description: Learn how LiquidJava checks recursive calls using parameter and return refinements.
+---
+
+# Recursion
+
+A recursive call is checked using the same parameter and return refinements as any other method call. LiquidJava uses the declared contract instead of repeatedly expanding the method body.
+
+```java
+import liquidjava.specification.Refinement;
+
+public class RecursionExample {
+    @Refinement("_ == 0")
+    public static int untilZero(
+            @Refinement("k >= 0") int k) {
+        if (k == 0) {
+            return 0;
+        } else {
+            return untilZero(k - 1);
+        }
+    }
+}
+```
+
+The verifier checks both branches:
+
+1. In the base case, returning `0` satisfies `_ == 0`.
+2. In the other branch, `k >= 0` and `k != 0` imply `k > 0`, since `k` is an integer. Therefore `k - 1 >= 0`, so the recursive call satisfies the parameter contract.
+3. The recursive call's return contract says its result equals `0`, which satisfies the enclosing method's return contract.
+
+## An Incorrect Base Case
+
+If the base case tests `k == 1`, the other branch can include `k == 0`. Subtracting one then violates the recursive call's parameter refinement:
+
+```java
+import liquidjava.specification.Refinement;
+
+public class IncorrectRecursionExample {
+    @Refinement("_ == 0")
+    public static int untilZero(
+            @Refinement("k >= 0") int k) {
+        if (k == 1) {
+            return 0;
+        } else {
+            // k could be 0, so k - 1 could be negative
+            return untilZero(k - 1); // Refinement Error
+        }
+    }
+}
+```
+
+{: .note }
+Checking recursive contracts does not prove termination or bound recursion depth. An accepted recursive method can still recurse forever or exhaust the Java stack. The return refinement describes the value if the method returns.
diff --git a/pages/vscode-extension/index.md b/pages/vscode-extension/index.md
index 8436ea3..ef000fe 100644
--- a/pages/vscode-extension/index.md
+++ b/pages/vscode-extension/index.md
@@ -1,6 +1,6 @@
 ---
 title: VS Code Extension
-nav_order: 4
+nav_order: 5
 has_children: true
 has_toc: false
 permalink: /vscode-extension/
diff --git a/scripts/playground/editor.js b/scripts/playground/editor.js
index f779d8b..0cadf31 100644
--- a/scripts/playground/editor.js
+++ b/scripts/playground/editor.js
@@ -126,7 +126,7 @@ document.querySelector('#lj-reset').onclick = reset;
 if (!crossOriginIsolated) {
   verify.disabled = true;
   if (!('serviceWorker' in navigator) || !isSecureContext) {
-    message('The playground requires HTTPS or localhost and service worker support.', 'failure');
+    message('The LiquidJava playground is not supported in this browser.', 'failure');
   } else {
     try {
       await navigator.serviceWorker.register(new URL('../isolation.js', runtime), { scope: new URL('../', runtime).pathname, updateViaCache: 'none' });