Import/export JSON for models and diagrams

packages/frontend/src/components/index.ts

@@ -11,3 +11,4 @@ export * from "./name_input";
 export * from "./panel";
 export * from "./resizable";
 export * from "./rich_text_editor";
+export * from "./json_import";

packages/frontend/src/components/json_import.css

@@ -0,0 +1,55 @@
+.json_import {
+    min-width: 20em;
+    max-width: 80vw;
+    margin: 0 auto;
+    padding: 1rem;
+    border: 1px solid #ccc;
+    border-radius: 8px;
+    background-color: #f9f9f9;
+    width: auto;
+}
+
+.json_import .flex {
+    display: flex;
+    flex-direction: column;
+    gap: 1rem;
+}
+
+.json_import label {
+    font-weight: 500;
+}
+
+.json_import input[type="file"] {
+    border: 1px solid #ccc;
+    padding: 0.5rem;
+    border-radius: 4px;
+}
+
+.json_import textarea {
+    border: 1px solid #ccc;
+    padding: 0.5rem;
+    border-radius: 4px;
+    font-family: monospace;
+    resize: vertical;
+    min-height: 10rem;
+    max-height: 80vh;
+}
+
+.json_import button {
+    padding: 0.5rem 1rem;
+    background-color: #007bff;
+    color: white;
+    border: none;
+    border-radius: 4px;
+    cursor: pointer;
+    transition: background-color 0.3s;
+}
+
+.json_import button:hover {
+    background-color: #0056b3;
+}
+
+.json_import .error {
+    color: red;
+    margin-top: 1rem;
+}

packages/frontend/src/components/json_import.tsx

@@ -0,0 +1,109 @@
+import { createSignal } from "solid-js";
+import type { Document } from "../api";
+import "./json_import.css";
+
+interface JsonImportProps<T extends string> {
+    onImport: (data: Document<T>) => void;
+    validate?: (data: Document<T>) => boolean | string;
+}
+
+export const JsonImport = <T extends string>(props: JsonImportProps<T>) => {
+    const [error, setError] = createSignal<string | null>(null);
+    const [pasteValue, setPasteValue] = createSignal("");
+
+    const handleError = (e: unknown) => {
+        setError(e instanceof Error ? e.message : "Unknown error occurred");
+    };
+
+    const validateAndImport = (jsonString: string) => {
+        try {
+            // Parse JSON
+            const data = JSON.parse(jsonString);
+
+            // Run custom validation if provided
+            if (props.validate) {
+                const validationResult = props.validate(data);
+                if (typeof validationResult === "string") {
+                    setError(validationResult);
+                    return;
+                }
+            }
+
+            // Clear any previous errors and import
+            setError(null);
+            props.onImport(data);
+            setPasteValue(""); // Clear paste area after successful import
+        } catch (e) {
+            handleError(e);
+        }
+    };
+
+    // Handle file upload
+    const handleFileUpload = async (event: Event) => {
+        const input = event.target as HTMLInputElement;
+        if (!input.files?.length) return;
+
+        try {
+            const file = input.files[0];
+
+            // Validate file type
+            if (!(file?.type === "application/json") && !file?.name.endsWith(".json")) {
+                throw new Error("Please upload a JSON file");
+            }
+
+            const MAX_FILE_SIZE = 5 * 1024 * 1024; // 5MB
+            if (file.size > MAX_FILE_SIZE) {
+                throw new Error("File size exceeds 5MB limit");
+            }
+
+            const text = await file?.text();
+            validateAndImport(text);
+
+            // Reset file input
+            input.value = "";
+        } catch (e) {
+            handleError(e);
+        }
+    };
+
+    // Handle paste
+    const handlePaste = () => {
+        if (!pasteValue().trim()) {
+            setError("Please enter some JSON");
+            return;
+        }
+        validateAndImport(pasteValue());
+    };
+
+    const handleInput = (event: Event) => {
+        const textarea = event.target as HTMLTextAreaElement;
+        setPasteValue(textarea.value);
+    };
+
+    return (
+        <div class="json_import">
+            {/* File upload */}
+            <div class="flex">
+                <label>Import from file:</label>
+                <input type="file" accept=".json,application/json" onChange={handleFileUpload} />
+            </div>
+
+            {/* JSON paste */}
+            <div class="flex">
+                <label>Or paste JSON:</label>
+                <textarea
+                    value={pasteValue()}
+                    onInput={handleInput}
+                    onPaste={handleInput}
+                    placeholder="Paste your JSON here..."
+                />
+                <button onClick={handlePaste} aria-label="Import JSON">
+                    Import Pasted JSON
+                </button>
+            </div>
+
+            {/* Error display */}
+            {error() && <div class="error">{error()}</div>}
+        </div>
+    );
+};

packages/frontend/src/diagram/diagram_menu.tsx

@@ -11,8 +11,12 @@ import {
     createDiagramFromDocument,
 } from "./document";
 
+import { copyToClipboard, downloadJson } from "../util/json_export";
+
 import ChartSpline from "lucide-solid/icons/chart-spline";
+import CopyToClipboard from "lucide-solid/icons/clipboard-copy";
 import Copy from "lucide-solid/icons/copy";
+import Export from "lucide-solid/icons/download";
 import FilePlus from "lucide-solid/icons/file-plus";
 
 /** Hamburger menu for a diagram in a model. */
@@ -59,6 +63,13 @@ export function DiagramMenuItems(props: {
         navigate(`/diagram/${newRef}`);
     };
 
+    //Can this be less repetitive?
+    const onDownloadJSON = (diagram: DiagramDocument) => {
+        downloadJson(JSON.stringify(diagram), `${diagram.name}.json`);
+    };
+    const onCopy = (diagram: DiagramDocument) => {
+        copyToClipboard(JSON.stringify(diagram));
+    };
     return (
         <>
             <MenuItem onSelect={() => onNewDiagram(props.liveDiagram.liveModel.refId)}>
@@ -74,6 +85,14 @@ export function DiagramMenuItems(props: {
                 <Copy />
                 <MenuItemLabel>{"Duplicate diagram"}</MenuItemLabel>
             </MenuItem>
+            <MenuItem onSelect={() => onDownloadJSON(props.liveDiagram.liveDoc.doc)}>
+                <Export />
+                <MenuItemLabel>{"Export notebook"}</MenuItemLabel>
+            </MenuItem>
+            <MenuItem onSelect={() => onCopy(props.liveDiagram.liveDoc.doc)}>
+                <CopyToClipboard />
+                <MenuItemLabel>{"Copy to clipboard"}</MenuItemLabel>
+            </MenuItem>
         </>
     );
 }

packages/frontend/src/model/model_menu.tsx

@@ -5,10 +5,13 @@ import { createAnalysis } from "../analysis/document";
 import { type StableRef, useApi } from "../api";
 import { createDiagram } from "../diagram/document";
 import { AppMenu, MenuItem, MenuItemLabel, MenuSeparator, NewModelItem } from "../page";
+import { copyToClipboard, downloadJson } from "../util/json_export";
 import { type LiveModelDocument, type ModelDocument, createModel } from "./document";
 
 import ChartSpline from "lucide-solid/icons/chart-spline";
+import CopyToClipboard from "lucide-solid/icons/clipboard-copy";
 import Copy from "lucide-solid/icons/copy";
+import Export from "lucide-solid/icons/download";
 import Network from "lucide-solid/icons/network";
 
 /** Hamburger menu for a model of a double theory. */
@@ -54,6 +57,12 @@ export function ModelMenuItems(props: {
         });
         navigate(`/model/${newRef}`);
     };
+    const onDownloadJSON = (model: ModelDocument) => {
+        downloadJson(JSON.stringify(model), `${model.name}.json`);
+    };
+    const onCopy = (model: ModelDocument) => {
+        copyToClipboard(JSON.stringify(model));
+    };
 
     return (
         <>
@@ -73,6 +82,14 @@ export function ModelMenuItems(props: {
                 <Copy />
                 <MenuItemLabel>{"Duplicate model"}</MenuItemLabel>
             </MenuItem>
+            <MenuItem onSelect={() => onDownloadJSON(props.liveModel.liveDoc.doc)}>
+                <Export />
+                <MenuItemLabel>{"Export notebook"}</MenuItemLabel>
+            </MenuItem>
+            <MenuItem onSelect={() => onCopy(props.liveModel.liveDoc.doc)}>
+                <CopyToClipboard />
+                <MenuItemLabel>{"Copy to clipboard"}</MenuItemLabel>
+            </MenuItem>
         </>
     );
 }

packages/frontend/src/page/import.tsx

@@ -0,0 +1,64 @@
+import { useNavigate } from "@solidjs/router";
+import invariant from "tiny-invariant";
+import { type Document, useApi } from "../api";
+import { JsonImport } from "../components";
+import { type DiagramDocument, createDiagramFromDocument } from "../diagram";
+import { type ModelDocument, createModel } from "../model";
+
+type ImportableDocument = ModelDocument | DiagramDocument;
+function isImportableDocument(doc: Document<string>): doc is ImportableDocument {
+    return doc.type === "model" || doc.type === "diagram";
+}
+
+export function Import(props: { onComplete?: () => void }) {
+    const api = useApi();
+    const navigate = useNavigate();
+    const handleImport = async (data: Document<string>) => {
+        invariant(
+            isImportableDocument(data),
+            "Analysis and other document types cannot be imported at this time.",
+        );
+
+        switch (data.type) {
+            case "model": {
+                const newRef = await createModel(api, data);
+                try {
+                    navigate(`/model/${newRef}`);
+                } catch (e) {
+                    throw new Error(`Failed to navigate to new ${data.type}: ${e}`);
+                }
+                break;
+            }
+
+            case "diagram": {
+                const newRef = await createDiagramFromDocument(api, data);
+                try {
+                    navigate(`/diagram/${newRef}`);
+                } catch (e) {
+                    throw new Error(`Failed to navigate to new ${data.type}: ${e}`);
+                }
+                break;
+            }
+
+            default:
+                throw new Error("Unknown document type");
+        }
+
+        props.onComplete?.();
+    };
+
+    // Placeholder, not doing more than typechecking does for now but
+    // will eventually validate against json schema
+    const validateJson = (data: Document<string>) => {
+        if (!isImportableDocument(data)) {
+            return "Analysis and other document types cannot be imported at this time.";
+        }
+        return true;
+    };
+
+    return (
+        <div>
+            <JsonImport<"model" | "diagram"> onImport={handleImport} validate={validateJson} />
+        </div>
+    );
+}

packages/frontend/src/page/menubar.tsx

@@ -9,14 +9,17 @@ import { useApi } from "../api";
 import { Dialog, IconButton } from "../components";
 import { createModel } from "../model/document";
 import { TheoryLibraryContext } from "../stdlib";
+
 import { Login } from "../user";
+import { Import } from "./import";
 
 import FilePlus from "lucide-solid/icons/file-plus";
 import Info from "lucide-solid/icons/info";
 import LogInIcon from "lucide-solid/icons/log-in";
 import LogOutIcon from "lucide-solid/icons/log-out";
 import MenuIcon from "lucide-solid/icons/menu";
 import SettingsIcon from "lucide-solid/icons/settings";
+import UploadIcon from "lucide-solid/icons/upload";
 
 import "./menubar.css";
 
@@ -57,16 +60,20 @@ export function AppMenu(props: {
     const auth = useAuth(getAuth(firebaseApp));
 
     const [loginOpen, setLoginOpen] = createSignal(false);
+    const [openImport, setImportOpen] = createSignal(false);
 
     // Root the dialog here so that it is not destroyed when the menu closes.
     return (
         <>
             <HamburgerMenu>
+                <ImportMenuItem showImport={() => setImportOpen(true)} />
                 {props.children}
                 <Show when={props.children}>
                     <MenuSeparator />
                 </Show>
+
                 <HelpMenuItem />
+
                 <Show
                     when={auth.data}
                     fallback={<LogInMenuItem showLogin={() => setLoginOpen(true)} />}
@@ -78,6 +85,9 @@ export function AppMenu(props: {
             <Dialog open={loginOpen()} onOpenChange={setLoginOpen} title="Log in">
                 <Login onComplete={() => setLoginOpen(false)} />
             </Dialog>
+            <Dialog open={openImport()} onOpenChange={setImportOpen} title="Import">
+                <Import onComplete={() => setImportOpen(false)} />
+            </Dialog>
         </>
     );
 }
@@ -154,3 +164,14 @@ function SettingsMenuItem() {
         </MenuItem>
     );
 }
+
+function ImportMenuItem(props: {
+    showImport: () => void;
+}) {
+    return (
+        <MenuItem onSelect={props.showImport}>
+            <UploadIcon />
+            <MenuItemLabel>{"Import notebook"}</MenuItemLabel>
+        </MenuItem>
+    );
+}