diff --git a/package-lock.json b/package-lock.json
index b659c92..b50e9f3 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -855,7 +855,6 @@
       "resolved": "https://registry.npmjs.org/@sveltejs/kit/-/kit-2.48.4.tgz",
       "integrity": "sha512-TGFX1pZUt9qqY20Cv5NyYvy0iLWHf2jXi8s+eCGsig7jQMdwZWKUFMR6TbvFNhfDSUpc1sH/Y5EHv20g3HHA3g==",
       "dev": true,
-      "peer": true,
       "dependencies": {
         "@standard-schema/spec": "^1.0.0",
         "@sveltejs/acorn-typescript": "^1.0.5",
@@ -894,7 +893,6 @@
       "resolved": "https://registry.npmjs.org/@sveltejs/vite-plugin-svelte/-/vite-plugin-svelte-5.1.1.tgz",
       "integrity": "sha512-Y1Cs7hhTc+a5E9Va/xwKlAJoariQyHY+5zBgCZg4PFWNYQ1nMN9sjK1zhw1gK69DuqVP++sht/1GZg1aRwmAXQ==",
       "dev": true,
-      "peer": true,
       "dependencies": {
         "@sveltejs/vite-plugin-svelte-inspector": "^4.0.1",
         "debug": "^4.4.1",
@@ -1195,7 +1193,6 @@
       "resolved": "https://registry.npmjs.org/acorn/-/acorn-8.15.0.tgz",
       "integrity": "sha512-NZyJarBfL7nWwIq+FDL6Zp/yHEhePMNnnJ0y3qfieCrmNvYct8uvtiV41UvlSe6apAfk0fY1FbWx+NwfmpvtTg==",
       "dev": true,
-      "peer": true,
       "bin": {
         "acorn": "bin/acorn"
       },
@@ -1469,7 +1466,6 @@
       "resolved": "https://registry.npmjs.org/picomatch/-/picomatch-4.0.3.tgz",
       "integrity": "sha512-5gTmgEY/sqK6gFXLIsQNH19lWb4ebPDLA4SdLP7dsWkIXHWlG66oPuVvXSGFPppYZz8ZDZq0dYYrbHfBCVUb1Q==",
       "dev": true,
-      "peer": true,
       "engines": {
         "node": ">=12"
       },
@@ -1510,7 +1506,6 @@
       "resolved": "https://registry.npmjs.org/prettier/-/prettier-3.8.1.tgz",
       "integrity": "sha512-UOnG6LftzbdaHZcKoPFtOcCKztrQ57WkHDeRD9t/PTQtmT0NHSeWWepj6pS0z/N7+08BHFDQVUrfmfMRcZwbMg==",
       "dev": true,
-      "peer": true,
       "bin": {
         "prettier": "bin/prettier.cjs"
       },
@@ -1631,7 +1626,6 @@
       "resolved": "https://registry.npmjs.org/svelte/-/svelte-5.43.5.tgz",
       "integrity": "sha512-HQoZArIewxQVNedseDsgMgnRSC4XOXczxXLF9rOJaPIJkg58INOPUiL8aEtzqZIXNSZJyw8NmqObwg/voajiHQ==",
       "dev": true,
-      "peer": true,
       "dependencies": {
         "@jridgewell/remapping": "^2.3.4",
         "@jridgewell/sourcemap-codec": "^1.5.0",
@@ -1705,7 +1699,6 @@
       "resolved": "https://registry.npmjs.org/typescript/-/typescript-5.6.3.tgz",
       "integrity": "sha512-hjcS1mhfuyi4WW8IWtjP7brDrG2cuDZukyrYrSauoXGNgx0S7zceP07adYkJycEr56BOUTNPzbInooiN3fn1qw==",
       "dev": true,
-      "peer": true,
       "bin": {
         "tsc": "bin/tsc",
         "tsserver": "bin/tsserver"
@@ -1719,7 +1712,6 @@
       "resolved": "https://registry.npmjs.org/vite/-/vite-6.4.1.tgz",
       "integrity": "sha512-+Oxm7q9hDoLMyJOYfUYBuHQo+dkAloi33apOPP56pzj+vsdJDzr+j1NISE5pyaAuKL4A3UD34qd0lx5+kfKp2g==",
       "dev": true,
-      "peer": true,
       "dependencies": {
         "esbuild": "^0.25.0",
         "fdir": "^6.4.4",
diff --git a/package.json b/package.json
index 0a48b24..2ef7d9c 100644
--- a/package.json
+++ b/package.json
@@ -31,4 +31,4 @@
     "typescript": "~5.6.2",
     "vite": "^6.0.3"
   }
-}
\ No newline at end of file
+}
diff --git a/src/lib/panel/Sequent.svelte b/src/lib/panel/Sequent.svelte
index c95673d..a8e37e3 100644
--- a/src/lib/panel/Sequent.svelte
+++ b/src/lib/panel/Sequent.svelte
@@ -1,14 +1,28 @@
 <script lang="ts">
     import TermTree from "$lib/components/TermTree.svelte";
+    import type {
+        Client,
+        NodeId,
+        NodeTextDesc,
+        ProofId,
+    } from "../../routes/api";
 
     let { appState } = $props();
 
-    let sequent = $state(null);
+    let sequent = $state<NodeTextDesc | null>(null);
+    let width = $state(120);
+    let contentEl: HTMLDivElement | null = $state(null);
+    let charWidthEstimatorEl: HTMLSpanElement | null = $state(null);
 
-    async function fetchSequent(client, proof, node) {
+    async function fetchSequent(
+        client: Client,
+        proof: ProofId,
+        node: NodeId,
+        width: number,
+    ) {
         const options = {
             unicode: false,
-            width: 120,
+            width,
             indentation: 0,
             pure: false,
             termLabels: true,
@@ -18,15 +32,34 @@
         return seq;
     }
 
+    $effect(() => {
+        if (!contentEl || !charWidthEstimatorEl) return;
+
+        const ro = new ResizeObserver((entries) => {
+            const px = entries[0].contentRect.width;
+            const charWidth = charWidthEstimatorEl?.offsetWidth!;
+            const newWidth = Math.floor(px / charWidth);
+
+            console.debug("resize to new width: " + newWidth);
+            width = newWidth;
+        });
+
+        ro.observe(contentEl);
+        return () => ro.disconnect();
+    });
+
     $effect(() => {
         if (appState.proof == null || appState.active_node == null) {
             return;
         }
 
+        const w = width;
+
         fetchSequent(
             appState.client,
             appState.proof,
             appState.active_node,
+            w,
         ).then((seq) => {
             sequent = seq;
         });
@@ -35,7 +68,15 @@
 
 <div class="sequent-container">
     <h3>Sequent</h3>
-    <div class="sequent-content">
+    <div class="sequent-content" bind:this={contentEl}>
+        <!-- This element is invisible and only exists so that we can extract
+        the character width, regardless of font size.
+        The character that we use for estimation does not matter; we use a monospace font.
+        -->
+        <code class="character-width-estimator" bind:this={charWidthEstimatorEl}
+            >x</code
+        >
+
         <!-- NOTE: That all of this is on a single line is deliberate: the pre element is whitespace/tab sensitive. -->
         <pre><code
                 >{#if sequent}{#key sequent}<TermTree {appState} {sequent} />
@@ -65,11 +106,17 @@
 
     pre {
         margin: 0;
-        white-space: pre-wrap;
-        word-wrap: break-word;
+        white-space: pre;
     }
 
     code {
         display: block;
     }
+
+    .character-width-estimator {
+        top: 0;
+        left: 0;
+        position: absolute;
+        visibility: hidden;
+    }
 </style>
diff --git a/src/routes/Header.svelte b/src/routes/Header.svelte
index 39cb241..d6e822a 100644
--- a/src/routes/Header.svelte
+++ b/src/routes/Header.svelte
@@ -2,7 +2,7 @@
     import ThemeToggle from "$lib/components/ThemeToggle.svelte";
     import Menu from "./Menu.svelte";
     import FilePicker from "./FilePicker.svelte";
-    import { open } from "@tauri-apps/plugin-fs";
+    import { save } from "@tauri-apps/plugin-dialog";
 
     let { appState, onError } = $props();
 
@@ -23,6 +23,25 @@
     function tryOpenKeyFile(path: string) {
         openKeyFile(path).catch((err) => onError(err.toString()));
     }
+    async function saveProofTo(path: string) {
+    await appState.client.saveProof(appState.proof, path);
+}
+
+async function onSaveProof() {
+    if (!appState.proof) {
+        onError("No proof loaded");
+        return;
+    }
+
+    const path = await save({
+        title: "Save proof",
+        defaultPath: "proof.proof",
+    });
+
+    if (!path) return; // user cancelled
+
+    saveProofTo(path).catch((err) => onError(err.toString()));
+}
 </script>
 
 <div class="header">
@@ -36,6 +55,9 @@
                             <FilePicker action={tryOpenKeyFile}>Open</FilePicker
                             >
                         </li>
+                        <li>
+                            <button onclick={onSaveProof}>Save</button>
+                        </li>
                     </ul>
                 </Menu>
             {/if}