ENH: Indicate validation errors in diagrams by angry red underline.

Author: epatters

packages/catlog/src/dbl/model_morphism.rs

@@ -404,12 +404,12 @@ pub enum InvalidDblModelMorphism<Ob, Mor> {
     #[error("Morphism `{0}` is not mapped to a morphism of the same type in the codomain")]
     MorType(Mor),
 
-    /// A morphism in the domain does not have dom preserved in codomain.
-    #[error("Morphism `{0}` domain not preserved in the codomain")]
+    /// Not functorial
+    #[error("Morphism `{0}` has domain not preserved by the mapping")]
     Dom(Mor),
 
-    /// A morphism in the domain does not have codom preserved in codomain
-    #[error("Morphism `{0}` codomain not preserved in the codomain")]
+    /// Not functorial
+    #[error("Morphism `{0}` has codomain not preserved by the mapping")]
     Cod(Mor),
 }
 

packages/frontend/src/diagram/morphism_cell_editor.tsx

@@ -31,6 +31,19 @@ export function DiagramMorphismCellEditor(props: {
     const domType = () => theory()?.theory.src(props.decl.morType);
     const codType = () => theory()?.theory.tgt(props.decl.morType);
 
+    const errors = () => {
+        const validated = liveDiagram.validatedDiagram();
+        if (validated?.result.tag !== "Err") {
+            return [];
+        }
+        return validated.result.content.filter((err) => err.err.content === props.decl.id);
+    };
+
+    const domInvalid = (): boolean =>
+        errors().some((err) => err.err.tag === "Dom" || err.err.tag === "DomType");
+    const codInvalid = (): boolean =>
+        errors().some((err) => err.err.tag === "Cod" || err.err.tag === "CodType");
+
     return (
         <div class="formal-judgment diagram-morphism-decl">
             <BasicObInput
@@ -43,6 +56,7 @@ export function DiagramMorphismCellEditor(props: {
                     });
                 }}
                 obType={domType()}
+                invalid={domInvalid()}
                 deleteForward={() => morRef()?.focus()}
                 exitBackward={() => morRef()?.focus()}
                 exitForward={() => codRef.focus()}
@@ -86,6 +100,7 @@ export function DiagramMorphismCellEditor(props: {
                     });
                 }}
                 obType={codType()}
+                invalid={codInvalid()}
                 deleteBackward={() => morRef()?.focus()}
                 exitBackward={() => domRef.focus()}
                 exitForward={props.actions.activateBelow}

packages/frontend/src/model/morphism_cell_editor.tsx

@@ -42,7 +42,7 @@ export function MorphismCellEditor(props: {
     ];
     const arrowClass = () => arrowStyles[morTypeMeta()?.arrowStyle ?? "default"];
 
-    const morphismErrors = () => {
+    const errors = () => {
         const validated = liveModel.validatedModel();
         if (validated?.result.tag !== "Err") {
             return [];
@@ -63,9 +63,7 @@ export function MorphismCellEditor(props: {
                         });
                     }}
                     obType={domType()}
-                    invalid={morphismErrors().some(
-                        (err) => err.tag === "Dom" || err.tag === "DomType",
-                    )}
+                    invalid={errors().some((err) => err.tag === "Dom" || err.tag === "DomType")}
                     deleteForward={() => nameRef()?.focus()}
                     exitBackward={() => nameRef()?.focus()}
                     exitForward={() => codRef.focus()}
@@ -110,9 +108,7 @@ export function MorphismCellEditor(props: {
                         });
                     }}
                     obType={codType()}
-                    invalid={morphismErrors().some(
-                        (err) => err.tag === "Cod" || err.tag === "CodType",
-                    )}
+                    invalid={errors().some((err) => err.tag === "Cod" || err.tag === "CodType")}
                     deleteBackward={() => nameRef()?.focus()}
                     exitBackward={() => domRef.focus()}
                     exitForward={props.actions.activateBelow}