BUG: Fix loss of reactivity caused by #682.

Author: epatters

packages/catlog-wasm/src/model.rs

@@ -487,15 +487,12 @@ pub fn collect_product(ob: Ob) -> Result<Vec<Ob>, String> {
 
 /// Elaborates a model defined by a notebook into a catlog model.
 #[wasm_bindgen(js_name = "elaborateModel")]
-pub fn elaborate_model(doc: &ModelDocumentContent, theory: &DblTheory) -> DblModel {
+pub fn elaborate_model(judgments: Vec<ModelJudgment>, theory: &DblTheory) -> DblModel {
     let mut model = DblModel::new(theory);
-
-    for cell in doc.notebook.cells() {
-        if let Cell::Formal { id: _, content } = cell {
-            match content {
-                ModelJudgment::Object(decl) => model.add_ob(decl).unwrap(),
-                ModelJudgment::Morphism(decl) => model.add_mor(decl).unwrap(),
-            }
+    for judgment in judgments {
+        match judgment {
+            ModelJudgment::Object(decl) => model.add_ob(&decl).unwrap(),
+            ModelJudgment::Morphism(decl) => model.add_mor(&decl).unwrap(),
         }
     }
     model

packages/catlog-wasm/src/model_diagram.rs

@@ -206,14 +206,12 @@ pub struct ModelDiagramValidationResult(
 
 /// Elaborates a diagram defined by a notebook into a catlog diagram.
 #[wasm_bindgen(js_name = "elaborateDiagram")]
-pub fn elaborate_diagram(doc: &DiagramDocumentContent, theory: &DblTheory) -> DblModelDiagram {
+pub fn elaborate_diagram(judgments: Vec<DiagramJudgment>, theory: &DblTheory) -> DblModelDiagram {
     let mut diagram = DblModelDiagram::new(theory);
-    for cell in doc.notebook.cells() {
-        if let Cell::Formal { id: _, content } = cell {
-            match content {
-                DiagramJudgment::Object(decl) => diagram.add_ob(decl).unwrap(),
-                DiagramJudgment::Morphism(decl) => diagram.add_mor(decl).unwrap(),
-            }
+    for judgment in judgments {
+        match judgment {
+            DiagramJudgment::Object(decl) => diagram.add_ob(&decl).unwrap(),
+            DiagramJudgment::Morphism(decl) => diagram.add_mor(&decl).unwrap(),
         }
     }
     diagram

packages/frontend/src/diagram/document.ts

@@ -1,5 +1,4 @@
 import { type Accessor, createMemo } from "solid-js";
-import { unwrap } from "solid-js/store";
 import invariant from "tiny-invariant";
 
 import type {
@@ -103,18 +102,14 @@ function enlivenDiagramDocument(
 
     const validatedDiagram = createMemo<ValidatedDiagram | undefined>(
         () => {
-            // NOTE: Reactively depend on formal judgments but, by `unwrap`-ing,
-            // not anything else in the document.
-            formalJudgments();
-
             const th = liveModel.theory();
             const validatedModel = liveModel.validatedModel();
             if (!(th && validatedModel?.result.tag === "Ok")) {
-                // Abort immediately if the model itself is invalid.
+                // Abort immediately if the theory is undefined or the model is invalid.
                 return undefined;
             }
             const { model } = validatedModel;
-            const diagram = elaborateDiagram(unwrap(doc), th.theory);
+            const diagram = elaborateDiagram(formalJudgments(), th.theory);
             diagram.inferMissingFrom(model);
             const result = diagram.validateIn(model);
             return { diagram, result };

packages/frontend/src/model/document.ts

@@ -1,5 +1,4 @@
 import { type Accessor, createMemo, createResource } from "solid-js";
-import { unwrap } from "solid-js/store";
 import invariant from "tiny-invariant";
 
 import {
@@ -107,13 +106,9 @@ function enlivenModelDocument(
 
     const validatedModel = createMemo<ValidatedModel | undefined>(
         () => {
-            // NOTE: Reactively depend on formal judgments but, by `unwrap`-ing,
-            // not anything else in the document.
-            formalJudgments();
-
             const coreTheory = theory()?.theory;
             if (coreTheory) {
-                const model = elaborateModel(unwrap(doc), coreTheory);
+                const model = elaborateModel(formalJudgments(), coreTheory);
                 const result = model.validate();
                 return { model, result };
             }
@@ -170,14 +165,12 @@ export async function migrateModelDocument(
     targetTheoryId: string,
     theories: TheoryLibrary,
 ) {
-    const theory = await theories.get(liveDoc.doc.theory);
+    const doc = liveDoc.doc;
+    const theory = await theories.get(doc.theory);
     const targetTheory = await theories.get(targetTheoryId);
 
     // Trivial migration.
-    if (
-        !NotebookUtils.hasFormalCells(liveDoc.doc.notebook) ||
-        theory.inclusions.includes(targetTheoryId)
-    ) {
+    if (!NotebookUtils.hasFormalCells(doc.notebook) || theory.inclusions.includes(targetTheoryId)) {
         liveDoc.changeDoc((doc) => {
             doc.theory = targetTheoryId;
         });
@@ -192,7 +185,7 @@ export async function migrateModelDocument(
     // TODO: We need a general method to propagate changes from catlog models to
     // notebooks. This stop-gap solution only works because pushforward
     // migration doesn't have to create/delete cells, only update types.
-    let model = elaborateModel(liveDoc.doc, theory.theory);
+    let model = elaborateModel(NotebookUtils.getFormalContent(doc.notebook), theory.theory);
     model = migration.migrate(model, targetTheory.theory);
     liveDoc.changeDoc((doc) => {
         doc.theory = targetTheoryId;