Add option to (not) centre tikz-cd output

src/dom.js

@@ -122,6 +122,11 @@ DOM.Element = class {
     bounding_rect() {
         return this.element.getBoundingClientRect();
     }
+
+    dispatch(event) {
+        this.element.dispatchEvent(event);
+        return this;
+    }
 };
 
 /// A class for conveniently dealing with SVGs.

src/main.css

@@ -517,7 +517,7 @@ being. */
 
     font-size: inherit;
     font-family: monospace;
-    color: hsl(0, 0%, 96%);
+    color: var(--ui-white);
 }
 
 .panel input[type="text"]::placeholder {
@@ -1200,7 +1200,7 @@ button.flash {
     background: hsla(50, 100%, 70%, 1);
 }
 
-.export .tip.hidden, .export .warning.hidden {
+.export .hidden {
     display: none;
 }
 
@@ -1210,6 +1210,59 @@ button.flash {
     list-style-type: circle;
 }
 
+.export .options {
+    margin-bottom: 8pt;
+    padding: 6pt 4pt;
+
+    background: var(--ui-black);
+    border-radius: 2px;
+
+    color: var(--ui-white);
+
+    user-select: none;
+    -webkit-user-select: none;
+}
+
+.export .options label {
+    position: relative;
+    top: 1px;
+}
+
+.export .options label kbd.hint {
+    /* Leave some space for the checkbox itself. */
+    transform: translate(-50%, -50%);
+}
+
+.export .options label input[type="checkbox"] {
+    margin-top: -1px;
+    margin-right: 6pt;
+    width: 12pt;
+    height: 12pt;
+    vertical-align: middle;
+
+    -webkit-appearance: none;
+    appearance: none;
+    background: var(--ui-white);
+    border-radius: 2px;
+    outline: none;
+}
+
+.export .options label input[type="checkbox"]:hover {
+    background: hsl(0, 0%, 80%);
+}
+
+.export .options label input[type="checkbox"]:checked {
+    background: var(--ui-focus);
+
+    text-align: center;
+}
+
+.export .options label input[type="checkbox"]:checked::before {
+    content: "✓";
+
+    color: var(--ui-black);
+}
+
 .export .code {
     font: 16px monospace;
     color: white;

src/quiver.js

@@ -174,12 +174,12 @@ class Quiver {
     /// Currently, the supported formats are:
     /// - "tikz-cd"
     /// - "base64"
-    export(format) {
+    export(format, settings) {
         switch (format) {
             case "tikz-cd":
-                return QuiverExport.tikz_cd.export(this);
+                return QuiverExport.tikz_cd.export(this, settings);
             case "base64":
-                return QuiverImportExport.base64.export(this);
+                return QuiverImportExport.base64.export(this, settings);
             default:
                 throw new Error(`unknown export format \`${format}\``);
         }
@@ -199,18 +199,21 @@ class QuiverImportExport extends QuiverExport {
 }
 
 QuiverExport.tikz_cd = new class extends QuiverExport {
-    export(quiver) {
+    export(quiver, settings) {
         let output = "";
 
         // Wrap tikz-cd code with `\begin{tikzcd} ... \end{tikzcd}`.
         // We also add custom TikZ styles if required, e.g. for drawing fixed-height curves, which
         // improve upon the build-in `bend` option.
         const wrap_boilerplate = (output) => {
-            const tikzcd = `\\[\\begin{tikzcd}\n${
+            let tikzcd = `\\begin{tikzcd}\n${
                 output.length > 0 ? `${
                     output.split("\n").map(line => `\t${line}`).join("\n")
                 }\n` : ""
-            }\\end{tikzcd}\\]`;
+            }\\end{tikzcd}`;
+            if (settings.get("export.centre_diagram")) {
+                tikzcd = `\\[${tikzcd}\\]`;
+            }
             return `% ${QuiverImportExport.base64.export(quiver).data}\n${tikzcd}`;
         };
 

src/ui.js

@@ -584,6 +584,9 @@ class UI {
 
         // The URL from which the macros have been fetched (if at all).
         this.macro_url = null;
+
+        // The user settings, which are stored persistently across sessions in `localStorage`.
+        this.settings = new Settings();
     }
 
     /// Reset most of the UI. We don't bother resetting current zoom, etc.: just enough to make
@@ -3257,6 +3260,35 @@ History.State = class {
     }
 };
 
+class Settings {
+    constructor() {
+        this.data = {
+            // Whether to wrap the `tikz-cd` output in `\[ \]`.
+            "export.centre_diagram": true,
+        };
+        try {
+            // Try to update the default values with the saved settings.
+            this.data = Object.assign(
+                this.data,
+                JSON.parse(window.localStorage.getItem("settings"))
+            );
+        } catch (_) {
+            // The JSON stored in `settings` was malformed.
+        }
+    }
+
+    /// Returns a saved user setting, or the default value if a setting has not been modified yet.
+    get(setting) {
+        return this.data[setting];
+    }
+
+    /// Saves a user setting.
+    set(setting, value) {
+        this.data[setting] = value;
+        window.localStorage.setItem("settings", JSON.stringify(this.data));
+    }
+}
+
 /// A panel for editing cell data.
 class Panel {
     constructor() {
@@ -3889,13 +3921,31 @@ class Panel {
             // If the user clicks on two different exports in a row
             // we will simply switch the displayed export format.
             // Clicking on the same button twice closes the panel.
-            if (this.export !== format) {
+            if (this.export === null || this.export.format !== format) {
                 ui.switch_mode(new UIMode.Modal());
 
                 // Get the encoding of the diagram. The output may be modified by the caller.
-                const { data, metadata } = modify(ui.quiver.export(format));
+                const { data, metadata } = modify(ui.quiver.export(format, ui.settings));
+
+                let export_pane, tip, warning, list, options, content;
+
+                const update_output = (data) => {
+                    // At present, the data is always a string.
+                    content.clear().add(data);
+                    // Select the code for easy copying.
+                    const select_output = () => {
+                        const selection = window.getSelection();
+                        const range = document.createRange();
+                        range.selectNodeContents(content.element);
+                        selection.removeAllRanges();
+                        selection.addRange(range);
+                    };
+                    select_output();
+                    // Safari seems to occasionally fail to select the text immediately, so we
+                    // also select it after a delay to ensure the text is selected.
+                    UI.delay(select_output);
+                };
 
-                let export_pane, tip, warning, list, content;
                 if (this.export === null) {
                     // Create the export pane.
                     export_pane = new DOM.Element("div", { class: "export" });
@@ -3930,14 +3980,48 @@ class Panel {
                             "appear in this diagram:")
                         .add(list = new DOM.Element("ul"))
                         .add_to(export_pane);
+
+                    const checkbox = new DOM.Element("input", { type: "checkbox" });
+                    options = new DOM.Element("div", { class: "options hidden" })
+                        .add(new DOM.Element("label")
+                            .add(checkbox)
+                            .add("Centre diagram")
+                        )
+                        .add_to(export_pane);
+
+                    // When the shortcut is active, we will always be displaying the modal pane,
+                    // so the shortcut is always valid.
+                    const shortcut = { key: "C", context: Shortcuts.SHORTCUT_PRIORITY.Always };
+                    new DOM.Element("kbd", { class: "hint button" })
+                        .add(Shortcuts.name([shortcut])).add_to(checkbox.parent);
+                    const shortcuts = [ui.shortcuts.add([shortcut], () => {
+                        if (!options.class_list.contains("hidden")) {
+                            checkbox.element.checked = !checkbox.element.checked;
+                            checkbox.dispatch(new Event("change"));
+                        }
+                    })];
+
+                    checkbox.listen("change", () => {
+                        ui.settings.set("export.centre_diagram", checkbox.element.checked);
+                        // Update the output. We ignore `metadata`, which currently does not change
+                        // in response to the settings.
+                        const { data } = modify(ui.quiver.export(format, ui.settings));
+                        update_output(data);
+                    });
+                    // Prevent the highlighted output from being deselected when changing a setting.
+                    checkbox.listen(pointer_event("up"), (event) => event.preventDefault());
+
                     content = new DOM.Element("div", { class: "code" }).add_to(export_pane);
                     ui.element.add(export_pane);
+
+                    this.export = { shortcuts };
                 } else {
                     // Find the existing export pane.
                     export_pane = ui.element.query_selector(".export");
                     tip = export_pane.query_selector(".tip");
                     warning = export_pane.query_selector(".warning");
                     list = export_pane.query_selector("ul");
+                    options = export_pane.query_selector(".options");
                     content = export_pane.query_selector(".code");
                 }
                 // Display a warning if necessary.
@@ -3951,18 +4035,18 @@ class Panel {
                 }
                 tip.class_list.toggle("hidden", format !== "tikz-cd");
                 warning.class_list.toggle("hidden", unsupported_items.length === 0);
+                options.class_list.toggle("hidden", format !== "tikz-cd");
 
-                // At present, the data is always a string.
-                content.clear().add(data);
+                const centre_checkbox = options.query_selector('input[type="checkbox"]');
+                if (ui.settings.get("export.centre_diagram")) {
+                    centre_checkbox.set_attributes({ checked: "" });
+                } else {
+                    centre_checkbox.remove_attributes("checked");
+                }
 
-                this.export = format;
+                this.export.format = format;
 
-                // Select the code for easy copying.
-                const selection = window.getSelection();
-                const range = document.createRange();
-                range.selectNodeContents(content.element);
-                selection.removeAllRanges();
-                selection.addRange(range);
+                update_output(data);
                 // Disable cell data editing while the export pane is visible.
                 this.update(ui);
             } else {
@@ -4475,6 +4559,9 @@ class Panel {
     dismiss_export_pane(ui) {
         if (this.export !== null) {
             ui.element.query_selector(".export").remove();
+            for (const id of this.export.shortcuts) {
+                ui.shortcuts.remove(id);
+            }
             this.export = null;
             ui.switch_mode(UIMode.default);
             this.update(ui);
@@ -4491,6 +4578,9 @@ class Shortcuts {
         // A map from keys to the shortcuts to which they correspond.
         this.shortcuts = new Map();
 
+        // An identifier for shortcuts, used to allow the caller to delete shortcuts.
+        this.next_id = 0;
+
         // Handle global key presses (such as, but not exclusively limited to, keyboard shortcuts).
         const handle_shortcut = (type, event) => {
             // Many keyboard shortcuts are only relevant when we're not midway
@@ -4592,6 +4682,7 @@ class Shortcuts {
                 this.shortcuts.set(key, []);
             }
             this.shortcuts.get(key).push({
+                id: this.next_id,
                 // `null` means we don't care about whether the modifier key
                 // is pressed or not, so we need to special case it.
                 modifier: shortcut.modifier !== null ? (shortcut.modifier || false) : null,
@@ -4604,6 +4695,14 @@ class Shortcuts {
                 button,
             });
         }
+        return this.next_id++;
+    }
+
+    // Remove all actions associated to a shortcut ID.
+    remove(id) {
+        for (const [key, shortcuts] of this.shortcuts) {
+            this.shortcuts.set(key, shortcuts.filter((shortcut) => shortcut.id !== id));
+        }
     }
 
     /// Returns whether this is likely to be an Apple platform or not, which determines what style