Import/export JSON for models and diagrams

packages/frontend/src/analysis/analysis_editor.tsx

@@ -15,9 +15,7 @@ import invariant from "tiny-invariant";
 import { useApi } from "../api";
 import { IconButton, ResizableHandle } from "../components";
 import { DiagramPane } from "../diagram/diagram_editor";
-import { DiagramMenuItems } from "../diagram/diagram_menu";
 import { ModelPane } from "../model/model_editor";
-import { ModelMenuItems } from "../model/model_menu";
 import {
     type CellConstructor,
     type FormalCellEditorProps,
@@ -38,6 +36,7 @@ import type { Analysis } from "./types";
 
 import PanelRight from "lucide-solid/icons/panel-right";
 import PanelRightClose from "lucide-solid/icons/panel-right-close";
+import { LiveDocumentMenuItems } from "../page/live_document_menu";
 
 export default function AnalysisPage() {
     const api = useApi();
@@ -142,24 +141,26 @@ export function AnalysisDocumentEditor(props: {
 
 const AnalysisMenu = (props: {
     liveAnalysis?: LiveAnalysisDocument;
-}) => (
-    <AppMenu disabled={props.liveAnalysis === undefined}>
-        <Switch>
-            <Match
-                when={props.liveAnalysis?.analysisType === "model" && props.liveAnalysis.liveModel}
-            >
-                {(liveModel) => <ModelMenuItems liveModel={liveModel()} />}
-            </Match>
-            <Match
-                when={
-                    props.liveAnalysis?.analysisType === "diagram" && props.liveAnalysis.liveDiagram
-                }
-            >
-                {(liveDiagram) => <DiagramMenuItems liveDiagram={liveDiagram()} />}
-            </Match>
-        </Switch>
-    </AppMenu>
-);
+}) => {
+    const liveDocument = (() => {
+        switch (props.liveAnalysis?.analysisType) {
+            case "diagram":
+                return props.liveAnalysis.liveDiagram;
+            case "model":
+                return props.liveAnalysis.liveModel;
+            default:
+                return undefined;
+        }
+    })();
+
+    return (
+        <AppMenu disabled={liveDocument === undefined}>
+            <Show when={liveDocument}>
+                {(liveDocument) => <LiveDocumentMenuItems liveDocument={liveDocument()} />}
+            </Show>
+        </AppMenu>
+    );
+};
 
 const AnalysisOfPane = (props: {
     liveAnalysis?: LiveAnalysisDocument;

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,120 @@
+import { ErrorBoundary, createSignal } from "solid-js";
+import type { JSX } from "solid-js";
+import type { Document } from "../api";
+import "./json_import.css";
+import { ErrorBoundaryDialog } from "../util/errors";
+
+interface JsonImportProps<T extends string> {
+    onImport: (data: Document<T>) => void;
+    validate?: (data: Document<T>) => boolean | string;
+}
+
+/**
+ * Component for importing JSON data.
+ * Handles file upload and direct clipboard paste.
+ * File size is currently limited to 5MB.
+ *
+ */
+export const JsonImport = <T extends string>({ onImport, validate }: JsonImportProps<T>) => {
+    const [error, setError] = createSignal<string | null>(null);
+    const [importValue, setImportValue] = createSignal("");
+
+    const handleError = (e: unknown) => {
+        setError(e instanceof Error ? e.message : "Unknown error occurred");
+    };
+
+    const validateAndImport = (jsonString: string) => {
+        try {
+            const data = JSON.parse(jsonString);
+
+            // Run custom validation if provided
+            if (validate) {
+                const validationResult = validate(data);
+                if (typeof validationResult === "string") {
+                    setError(validationResult);
+                    return;
+                }
+            }
+
+            // Clear any previous errors and import
+            setError(null);
+            onImport(data);
+            setImportValue(""); // Clear paste area after successful import
+        } catch (e) {
+            handleError(e);
+        }
+    };
+
+    // Handle file upload
+    const handleFileUpload: JSX.EventHandler<HTMLInputElement, Event> = async (event) => {
+        const input = event.currentTarget;
+
+        const file = input.files?.[0];
+        if (!file) return;
+
+        // Validate file type
+        if (file.type !== "application/json" && !file.name.endsWith(".json")) {
+            setError("Please upload a JSON file");
+            return;
+        }
+
+        const MAX_FILE_SIZE = 5 * 1024 * 1024; // 5MB
+        if (file.size > MAX_FILE_SIZE) {
+            setError("File size exceeds 5MB limit");
+            return;
+        }
+
+        const text = await file.text();
+        validateAndImport(text);
+
+        // Reset file input
+        input.value = "";
+    };
+
+    // Handle paste
+    const handleTextareaSubmit = () => {
+        if (!importValue().trim()) {
+            setError("Please enter some JSON");
+            return;
+        }
+        validateAndImport(importValue());
+    };
+
+    const handleInput: JSX.EventHandler<HTMLTextAreaElement, Event> = (event) => {
+        const textarea = event.currentTarget;
+        setImportValue(textarea.value);
+    };
+
+    return (
+        <div class="json_import">
+            <ErrorBoundary fallback={(err) => <ErrorBoundaryDialog error={err} />}>
+                {/* 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={importValue()}
+                        onInput={handleInput}
+                        onPaste={handleInput}
+                        placeholder="Paste your JSON here..."
+                    />
+                    <button onClick={handleTextareaSubmit} aria-label="Import JSON">
+                        Import Pasted JSON
+                    </button>
+                </div>
+
+                {/* Error display */}
+                {error() && <div class="error">{error()}</div>}
+            </ErrorBoundary>
+        </div>
+    );
+};

packages/frontend/src/diagram/diagram_editor.tsx

@@ -18,7 +18,6 @@ import { TheoryLibraryContext } from "../stdlib";
 import type { InstanceTypeMeta } from "../theory";
 import { MaybePermissionsButton } from "../user";
 import { LiveDiagramContext } from "./context";
-import { DiagramMenu } from "./diagram_menu";
 import { type LiveDiagramDocument, getLiveDiagram } from "./document";
 import { DiagramMorphismCellEditor } from "./morphism_cell_editor";
 import { DiagramObjectCellEditor } from "./object_cell_editor";
@@ -32,6 +31,7 @@ import {
 } from "./types";
 
 import "./diagram_editor.css";
+import { LiveDocumentMenu } from "../page/live_document_menu";
 
 export default function DiagramPage() {
     const api = useApi();
@@ -54,7 +54,7 @@ export function DiagramDocumentEditor(props: {
     return (
         <div class="growable-container">
             <Toolbar>
-                <DiagramMenu liveDiagram={props.liveDiagram} />
+                <LiveDocumentMenu liveDocument={props.liveDiagram} />
                 <span class="filler" />
                 <TheoryHelpButton theory={props.liveDiagram?.liveModel.theory()} />
                 <MaybePermissionsButton

packages/frontend/src/diagram/document.ts

@@ -40,6 +40,9 @@ export const newDiagramDocument = (modelRef: StableRef): DiagramDocument => ({
 /** A diagram document "live" for editing.
  */
 export type LiveDiagramDocument = {
+    /** discriminator for use in union types */
+    type: "diagram";
+
     /** The ref for which this is a live document. */
     refId: string;
 
@@ -122,7 +125,15 @@ function enlivenDiagramDocument(
         { equals: false },
     );
 
-    return { refId, liveDoc, liveModel, formalJudgments, objectIndex, validatedDiagram };
+    return {
+        type: "diagram",
+        refId,
+        liveDoc,
+        liveModel,
+        formalJudgments,
+        objectIndex,
+        validatedDiagram,
+    };
 }
 
 /** Create a new, empty diagram in the backend. */

packages/frontend/src/model/document.ts

@@ -32,6 +32,9 @@ export const newModelDocument = (theory: string): ModelDocument => ({
 Contains a live document for the model, plus various memos of derived data.
  */
 export type LiveModelDocument = {
+    /** discriminator for use in union types */
+    type: "model";
+
     /** The ref for which this is a live document. */
     refId: string;
 
@@ -111,6 +114,7 @@ function enlivenModelDocument(
     );
 
     return {
+        type: "model",
         refId,
         liveDoc,
         formalJudgments,