From bc7f052fc6b5101eed95c92e434c9ae381d510ce Mon Sep 17 00:00:00 2001 From: Kaspar Bumke Date: Tue, 28 Apr 2026 16:44:46 +0100 Subject: [PATCH 1/6] FIX: tsify output for `Composite` --- packages/document-types/src/v0/model.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/packages/document-types/src/v0/model.rs b/packages/document-types/src/v0/model.rs index 6ad4ad26a..edb8c381e 100644 --- a/packages/document-types/src/v0/model.rs +++ b/packages/document-types/src/v0/model.rs @@ -33,7 +33,7 @@ pub enum Mor { Basic(String), /// Composite of morphisms. - Composite(Box>), + Composite(#[tsify(type = "Path")] Box>), /// Morphism between tabulated morphisms, a commutative square. TabulatorSquare { From 956b26864bed6e89d98985e5aafeb6cefaac9ab1 Mon Sep 17 00:00:00 2001 From: Kaspar Bumke Date: Wed, 29 Apr 2026 14:06:55 +0100 Subject: [PATCH 2/6] ENH: Add list_simple_paths method to catlog --- packages/catlog-wasm/src/model.rs | 60 +++++++++++++- packages/catlog/src/one/graph_algorithms.rs | 92 +++++++++++++++++++++ 2 files changed, 151 insertions(+), 1 deletion(-) diff --git a/packages/catlog-wasm/src/model.rs b/packages/catlog-wasm/src/model.rs index 7dae0666c..fb8631963 100644 --- a/packages/catlog-wasm/src/model.rs +++ b/packages/catlog-wasm/src/model.rs @@ -19,7 +19,9 @@ use catlog::dbl::{ }, theory::{self as dbl_theory, ModalObOp, NonUnital, Unital}, }; -use catlog::one::{Category as _, FgCategory, Path, QualifiedPath}; +use catlog::one::{ + Category as _, FgCategory, Path, QualifiedPath, graph_algorithms::bounded_simple_paths_all, +}; use catlog::tt::{ self, notebook_elab::{Elaborator as ElaboratorNext, demote_modality, promote_modality}, @@ -584,6 +586,20 @@ impl DblModel { }) } + /// Lists all simple paths in the model. + #[wasm_bindgen(js_name = "listSimplePaths")] + pub fn list_simple_paths(&self, max_length: Option) -> Result, String> { + match &self.model { + DblModelBox::Discrete(model) => { + let graph = model.generating_graph(); + let paths = + bounded_simple_paths_all(graph, max_length).map(|p| Quoter.quote(&p)).collect(); + Ok(paths) + } + _ => Err("listSimplePaths is only supported on discrete double models".into()), + } + } + /// Gets the human-readable label, if any, for an object generator. #[wasm_bindgen(js_name = "obGeneratorLabel")] pub fn ob_generator_label(&self, id: &QualifiedName) -> Option { @@ -918,4 +934,46 @@ pub(crate) mod tests { assert_eq!(model.mor_generators().len(), 2); assert_eq!(model.validate().0, JsResult::Ok(())); } + + #[test] + fn list_simple_paths_basic() { + let th = ThSchema::new().theory(); + let [a, entity, attr_type] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()]; + let model = sch_walking_attr(&th, [a, entity, attr_type]); + + let paths = model.list_simple_paths(None).expect("should succeed"); + + // Identity at entity + identity at attr_type + the single morphism `a`. + assert_eq!(paths.len(), 3); + // The basic morphism appears in the result. + assert!(paths.iter().any(|p| matches!(p, Mor::Basic(id) if id == &a.to_string()))); + // Two identity paths appear in the result. + let id_count = paths + .iter() + .filter(|p| { + matches!( + p, + Mor::Composite(boxed) if matches!(boxed.as_ref(), notebook_path::Path::Id(_)) + ) + }) + .count(); + assert_eq!(id_count, 2); + + // max_length = 0 yields only the two identity paths. + let paths_zero = model.list_simple_paths(Some(0)).expect("should succeed"); + assert_eq!(paths_zero.len(), 2); + } + + #[test] + fn list_simple_paths_non_discrete() { + // Modal theory ⇒ listSimplePaths should error. + let th = ThSymMonoidalCategory::new().theory(); + let model = DblModel::new(&th); + let result = model.list_simple_paths(None); + let err = result.expect_err("expected error for non-discrete model"); + assert!( + err.contains("only supported on discrete double models"), + "unexpected error: {err}" + ); + } } diff --git a/packages/catlog/src/one/graph_algorithms.rs b/packages/catlog/src/one/graph_algorithms.rs index 3ef0d58ce..88de2c8f6 100644 --- a/packages/catlog/src/one/graph_algorithms.rs +++ b/packages/catlog/src/one/graph_algorithms.rs @@ -93,6 +93,24 @@ where maybe_empty_path.into_iter().chain(nonempty_paths) } +/// Iterates over all simple paths of bounded length in a finite graph. +pub fn bounded_simple_paths_all<'a, G>( + graph: &'a G, + max_length: Option, +) -> impl Iterator> + 'a +where + G: FinGraph, + G::V: Hash, + G::E: Hash, +{ + let vertices: Vec = graph.vertices().collect(); + vertices.clone().into_iter().flat_map(move |from| { + vertices.clone().into_iter().flat_map(move |to| { + bounded_simple_paths(graph, &from.clone(), &to, max_length).collect::>() + }) + }) +} + /// Arrange all the elements of a finite graph in specialization order. /// /// The [specialization @@ -390,6 +408,80 @@ mod tests { assert_eq!(paths, target); } + #[test] + fn find_simple_paths_all() { + // Triangle: edge 0: 0->1, edge 1: 1->2, edge 2: 0->2. + let g = SkelGraph::triangle(); + let paths: Vec<_> = bounded_simple_paths_all(&g, None).collect(); + let paths_set: HashSet<_> = paths.iter().cloned().collect(); + let expected: HashSet<_> = HashSet::from([ + // Identity paths at each vertex. + Path::Id(0), + Path::Id(1), + Path::Id(2), + // Non-identity simple paths from 0. + Path::single(0), // 0 -> 1 + Path::single(2), // 0 -> 2 (diagonal) + Path::pair(0, 1), // 0 -> 1 -> 2 + // Non-identity simple paths from 1. + Path::single(1), /* 1 -> 2 + * No non-identity paths from 2 (no out-edges). */ + ]); + assert_eq!(paths_set, expected); + // Vertices are visited in order, identity emitted first per vertex. + assert_eq!( + paths.iter().filter(|p| matches!(p, Path::Id(_))).cloned().collect::>(), + vec![Path::Id(0), Path::Id(1), Path::Id(2)] + ); + + // max_length restricts edge count, but identity paths at every vertex + // are always emitted. + // 3 identities only. + assert_eq!(bounded_simple_paths_all(&g, Some(0)).count(), 3); + // 3 identities + 3 single-edge paths (0->1, 0->2, 1->2). + assert_eq!(bounded_simple_paths_all(&g, Some(1)).count(), 6); + // ...plus the 0 -> 1 -> 2 pair. + assert_eq!(bounded_simple_paths_all(&g, Some(2)).count(), 7); + + // Cycle terminates due to simple-path semantics. + let g = SkelGraph::cycle(3); + let paths: HashSet<_> = bounded_simple_paths_all(&g, None).collect(); + let expected: HashSet<_> = HashSet::from([ + // Identity paths. + Path::Id(0), + Path::Id(1), + Path::Id(2), + // From 0: 0, 0;1, 0;1;2. + Path::single(0), + Path::pair(0, 1), + Path::Seq(nonempty![0, 1, 2]), + // From 1: 1, 1;2, 1;2;0. + Path::single(1), + Path::pair(1, 2), + Path::Seq(nonempty![1, 2, 0]), + // From 2: 2, 2;0, 2;0;1. + Path::single(2), + Path::pair(2, 0), + Path::Seq(nonempty![2, 0, 1]), + ]); + assert_eq!(paths, expected); + + // Self-loops are simple paths of length 1. + let mut g: HashGraph<_, _> = Default::default(); + assert!(g.add_vertex('x')); + assert!(g.add_edge('f', 'x', 'x')); + assert!(g.add_edge('g', 'x', 'x')); + let paths: HashSet<_> = bounded_simple_paths_all(&g, None).collect(); + let expected: HashSet<_> = HashSet::from([ + Path::Id('x'), + Path::Seq(nonempty!['f']), + Path::Seq(nonempty!['g']), + Path::Seq(nonempty!['f', 'g']), + Path::Seq(nonempty!['g', 'f']), + ]); + assert_eq!(paths, expected); + } + #[test] fn toposorting() { let g = SkelGraph::path(5); From abe78d08aa2c9d00193764157163921770554513 Mon Sep 17 00:00:00 2001 From: Kaspar Bumke Date: Fri, 8 May 2026 13:32:06 +0100 Subject: [PATCH 3/6] ENH: Add equation cell editor UI --- packages/document-methods/src/model.ts | 9 + packages/frontend/src/model/editors.ts | 11 +- .../src/model/equation_cell_editor.module.css | 171 ++++ .../src/model/equation_cell_editor.tsx | 900 ++++++++++++++++++ packages/frontend/src/model/model_editor.tsx | 35 +- .../src/stdlib/theories/simple-olog.ts | 5 + .../src/stdlib/theories/simple-schema.ts | 5 + packages/frontend/src/theory/theory.ts | 28 + .../ui-components/src/completions.stories.tsx | 62 ++ packages/ui-components/src/completions.tsx | 142 ++- packages/ui-components/src/inline_input.tsx | 12 +- packages/ui-components/src/text_input.tsx | 76 +- 12 files changed, 1402 insertions(+), 54 deletions(-) create mode 100644 packages/frontend/src/model/equation_cell_editor.module.css create mode 100644 packages/frontend/src/model/equation_cell_editor.tsx diff --git a/packages/document-methods/src/model.ts b/packages/document-methods/src/model.ts index 2fe244d67..1c2618689 100644 --- a/packages/document-methods/src/model.ts +++ b/packages/document-methods/src/model.ts @@ -38,6 +38,15 @@ export const newMorphismDecl = (morType: MorType): ModelJudgment & { tag: "morph cod: null, }); +/** Create a new equation declaration. */ +export const newEquationDecl = (): ModelJudgment & { tag: "equation" } => ({ + tag: "equation", + id: v7(), + name: "", + lhs: null, + rhs: null, +}); + /** Create a new instantiation of an existing model. */ export const newInstantiatedModel = ( model?: Link | null, diff --git a/packages/frontend/src/model/editors.ts b/packages/frontend/src/model/editors.ts index 131d8595a..35fd40791 100644 --- a/packages/frontend/src/model/editors.ts +++ b/packages/frontend/src/model/editors.ts @@ -1,7 +1,7 @@ import type { Component } from "solid-js"; import type { FocusHandle } from "catcolab-ui-components"; -import type { MorDecl, ObDecl } from "catlog-wasm"; +import type { EqnDecl, MorDecl, ObDecl } from "catlog-wasm"; import type { CellActions } from "../notebook"; import type { Theory } from "../theory"; import type { MorTypeMap, ObTypeMap } from "../theory/types"; @@ -33,3 +33,12 @@ export type MorphismEditorProps = { actions: CellActions; theory: Theory; }; + +/** Props for an equation cell editor component in a model. */ +export type EquationEditorProps = { + equation: EqnDecl; + modifyEquation: (f: (decl: EqnDecl) => void) => void; + focus: FocusHandle; + actions: CellActions; + theory: Theory; +}; diff --git a/packages/frontend/src/model/equation_cell_editor.module.css b/packages/frontend/src/model/equation_cell_editor.module.css new file mode 100644 index 000000000..6bb2086dd --- /dev/null +++ b/packages/frontend/src/model/equation_cell_editor.module.css @@ -0,0 +1,171 @@ +.decl { + display: flex; + flex-direction: column; + align-items: stretch; + gap: 0.5em; + margin-bottom: 1em; + margin-right: 1em; +} + +.body { + display: flex; + flex-direction: column; + gap: 0.5em; + position: relative; + margin-left: 0.5rem; + padding-left: 1rem; + + &:before { + content: ""; + position: absolute; + left: 0; + top: 0; + bottom: 0; + width: 2px; + background: var(--color-gray-450); + } +} + +.name { + /* Match the look of a morphism cell's name: a plain `NameInput` rendered + at the surrounding `formal-judgment` font size, with no extra styling. */ + display: inline-flex; + align-items: baseline; +} + +.pathPicker { + display: flex; + flex-direction: row; + align-items: center; + justify-content: center; + gap: 1ex; + width: 100%; + min-width: 0; + box-sizing: border-box; + padding: 0.75em 1em; + cursor: text; + min-height: 90px; +} + +.equals { + font-size: 1.5em; + text-align: center; + line-height: 1; +} + +.pathDisplay { + cursor: text; + display: block; + min-width: 0; +} + +.path { + display: flex; + flex-direction: row; + flex-wrap: wrap; + align-items: center; + justify-content: center; + gap: 1ex; + min-width: 0; + box-sizing: border-box; + /* Vertical room for morphism names above arrows; see arrow_styles.module.css. */ + --formal-judgment-font-size: 0.9em; + line-height: 1.2; +} + +/* A single (arrow + cod object) segment, kept together as one wrappable unit + so the arrow never lands on a different line than its codomain. */ +.segment { + display: inline-flex; + flex-direction: row; + align-items: center; + gap: 1ex; +} + +.object { + /* Aligned with `.morphism-decl-dom`/`.morphism-decl-cod` styling. */ + display: inline-flex; + align-items: center; +} + +.morName { + /* Aligned with `.morphism-decl-name` styling. */ + text-align: center; +} + +/* Mid-path ellipsis used when abbreviating long paths. Sits inline between + adjacent (arrow + cod object) segments. */ +.ellipsis { + display: inline-flex; + align-items: center; + padding: 0 0.25em; +} + +/* A single completion row: typeable name on top as a caption, diagrammatic + path beneath. The whole row is supplied via `renderItem` and replaces the + default `` row layout, so the box is drawn here rather than + on the surrounding `
  • `. */ +.completionRow { + display: flex; + flex-direction: column; + gap: 1.25em; + min-width: 0; + border: 1px solid var(--color-gray-300, #ddd); + border-radius: 4px; + padding: 0.75em 1em; + background: var(--color-bg, transparent); +} + +.completionName { + /* Inherit the surrounding font (matches the InlineInput) instead of + using a monospace face. */ + font-size: 1em; + text-align: center; + + & > span { + display: inline-block; + max-width: 100%; + white-space: nowrap; + overflow: hidden; + text-overflow: ellipsis; + } +} + +.completionsPopup { + font-size: 1.3em; + line-height: 1.1; + min-width: 24em; + max-width: 40em; + padding: 0.5rem; + + & :global(.completion-list) { + display: flex; + flex-direction: column; + gap: 0.5em; + } + + /* The per-row box draws its own padding, so suppress the default per-li + padding and let the box reach the list edges. */ + & :global(.completion-list li) { + padding: 0; + } +} + +.unnamed { + font-style: italic; + color: var(--color-gray-600, #777); +} + +.error { + color: var(--color-red-500, red); + font-size: 0.9em; +} + +.unresolved { + border-bottom: 2px solid var(--color-inline-input-warning); +} + +.clearButton { + display: inline-flex; + align-items: center; +} diff --git a/packages/frontend/src/model/equation_cell_editor.tsx b/packages/frontend/src/model/equation_cell_editor.tsx new file mode 100644 index 000000000..4a1299fed --- /dev/null +++ b/packages/frontend/src/model/equation_cell_editor.tsx @@ -0,0 +1,900 @@ +import { deepEqual } from "fast-equals"; +import X from "lucide-solid/icons/x"; +import { For, Show, createEffect, createMemo, createSignal, useContext } from "solid-js"; +import invariant from "tiny-invariant"; +import { P, match } from "ts-pattern"; + +import { + type Completion, + type FocusHandle, + IconButton, + InlineInput, + NameInput, + useChildFocus, +} from "catcolab-ui-components"; +import type { DblModel, Mor, MorType, Ob, ObType, QualifiedLabel } from "catlog-wasm"; +import type { Theory } from "../theory"; +import { LiveModelContext } from "./context"; +import type { EquationEditorProps } from "./editors"; +import { obClasses } from "./object_cell_editor"; + +import arrowStyles from "../stdlib/arrow_styles.module.css"; +import styles from "./equation_cell_editor.module.css"; + +type EquationCellInput = "name" | "lhs" | "rhs"; + +/** Extract the object an identity path is at, if `mor` is an identity path. */ +function identityPathObject(mor: Mor): Ob | null { + return match(mor) + .with({ tag: "Composite", content: { tag: "Id", content: P.select() } }, (ob) => ob) + .otherwise(() => null); +} + +/** Number of edges in a simple-path morphism: 0 for identities, 1 for a basic + morphism, n for `Mor::Composite(Path::Seq(xs))`. Other shapes return + `Number.POSITIVE_INFINITY` so they sort last. */ +function pathLength(mor: Mor): number { + return match(mor) + .with({ tag: "Composite", content: { tag: "Id" } }, () => 0) + .with({ tag: "Basic" }, () => 1) + .with({ tag: "Composite", content: { tag: "Seq", content: P.select() } }, (xs) => xs.length) + .otherwise(() => Number.POSITIVE_INFINITY); +} + +/** Extract the basic-object id from an Ob, if it is a basic object. */ +function basicObId(ob: Ob | null): string | null { + return match(ob) + .with({ tag: "Basic", content: P.select() }, (id) => id) + .otherwise(() => null); +} + +/** Compute the domain object of a morphism using the model. */ +function morDom(model: DblModel | undefined, mor: Mor | null): Ob | null { + if (!model || !mor) { + return null; + } + try { + return model.dom(mor); + } catch { + return null; + } +} + +/** Compute the codomain object of a morphism using the model. */ +function morCod(model: DblModel | undefined, mor: Mor | null): Ob | null { + if (!model || !mor) { + return null; + } + try { + return model.cod(mor); + } catch { + return null; + } +} + +/** Typeable text for a path: morphism labels joined by `;`, or `id(Object)` + for an identity. Returns `""` if the path can't be presented. */ +function formatPathName(labels: string[]): string { + return labels.join(" ; "); +} + +function normalizePathName(text: string): string { + return text + .replace(/\s*;\s*/g, ";") + .trim() + .toLowerCase(); +} + +function pathText(model: DblModel | undefined, mor: Mor | null): string { + if (!model || !mor) { + return ""; + } + const idOb = identityPathObject(mor); + if (idOb !== null) { + return identityText(model, idOb); + } + const segs = describePath(model, mor); + return segs ? formatPathName(segs.morphisms.map((s) => s.label || "Unnamed")) : ""; +} + +/** Editor for an equation cell in a model. + +Layout: `[name] [lhs path picker] = [rhs path picker]`. + +Each path picker shows a typeable list of every simple path in the model as +completions, each rendered diagrammatically. + */ +export default function EquationCellEditor(props: EquationEditorProps) { + const liveModel = useContext(LiveModelContext); + invariant(liveModel, "Live model should be provided as context"); + + // oxlint-disable-next-line solid/reactivity -- Focus handles are stable for a mounted cell. + const focus = useChildFocus(props.focus, { default: "name" }); + + const elaborated = (): DblModel | undefined => liveModel().elaboratedModel(); + + const setLhs = (mor: Mor | null) => + props.modifyEquation((eqn) => { + eqn.lhs = mor; + }); + + const setRhs = (mor: Mor | null) => + props.modifyEquation((eqn) => { + eqn.rhs = mor; + }); + + const setName = (name: string) => + props.modifyEquation((eqn) => { + eqn.name = name; + }); + + /** All simple paths in the model, including identities, sorted by edge + count (shortest first); ties broken by the iteration order from the + wasm. */ + const allPaths = createMemo(() => { + const m = elaborated(); + if (!m) { + return []; + } + try { + const paths = m.listSimplePaths(undefined); + return paths + .map((mor, i) => ({ mor, i, len: pathLength(mor) })) + .toSorted((a, b) => a.len - b.len || a.i - b.i) + .map((x) => x.mor); + } catch { + return []; + } + }); + + /** Paths available for the RHS picker. + + When LHS has dom/cod we prioritize paths with matching dom/cod first. + */ + const rhsPaths = createMemo(() => { + const m = elaborated(); + const paths = allPaths(); + const dom = morDom(m, props.equation.lhs); + const cod = morCod(m, props.equation.lhs); + if (!m || dom === null || cod === null) { + return paths; + } + + const prioritized: Mor[] = []; + const rest: Mor[] = []; + for (const mor of paths) { + const d = morDom(m, mor); + const c = morCod(m, mor); + if (d !== null && c !== null && deepEqual(d, dom) && deepEqual(c, cod)) { + prioritized.push(mor); + } else { + rest.push(mor); + } + } + return prioritized.concat(rest); + }); + + return ( +
    +
    + focus.setActiveChild("lhs")} + exitUp={props.actions.activateAbove} + exitDown={() => focus.setActiveChild("lhs")} + exitRight={() => focus.setActiveChild("lhs")} + createBelow={() => focus.setActiveChild("lhs")} + /> +
    +
    + setActiveInput("name")} + exitForward={() => setActiveInput("rhs")} + exitUp={() => setActiveInput("name")} + exitDown={() => setActiveInput("rhs")} + exitLeft={() => setActiveInput("name")} + exitRight={() => setActiveInput("rhs")} + hasFocused={() => { + setActiveInput("lhs"); + props.actions.hasFocused?.(); + }} + createBelow={() => setActiveInput("rhs")} + /> +
    {"="}
    + setActiveInput("lhs")} + exitForward={props.actions.activateBelow} + exitUp={() => focus.setActiveChild("lhs")} + exitDown={props.actions.activateBelow} + exitLeft={() => focus.setActiveChild("lhs")} + exitRight={props.actions.activateBelow} + createBelow={props.actions.activateBelow} + /> +
    +
    + ); +} + +type PathPickerProps = { + model: DblModel | undefined; + theory: Theory; + paths: Mor[]; + mor: Mor | null; + setMor: (mor: Mor | null) => void; + isActive: boolean; + exitBackward?: () => void; + exitForward?: () => void; + exitUp?: () => void; + exitDown?: () => void; + exitLeft?: () => void; + exitRight?: () => void; + createBelow?: () => void; +}; + +/** Picker for a path in the model. + +When inactive and a path is set, renders the path diagrammatically +(`A —f→ B —g→ C`). When active, an `InlineInput` is shown with the supplied +list of paths as completions; a custom filter recognises path-syntax +conventions (`id(Foo)`, `f ; g`) and a custom renderer draws each completion +diagrammatically. + +The picker keeps the last unresolved typed text (i.e. text the user typed +that didn't match any path) in a parent-owned signal, so re-entering edit +mode re-populates the input with what was typed before. + */ +function PathPicker(props: PathPickerProps) { + const [unresolvedText, setUnresolvedText] = createSignal(null); + + /** Resolution-relevant data for each available path: enough to render a + completion row, filter, and resolve typed text. The active input + wraps these into full `Completion` items by attaching its + `onComplete` closure. Hoisted to the parent so re-association can + run while the input is unmounted. */ + const entries = createMemo(() => { + const m = props.model; + if (!m) { + return []; + } + const out: PathEntry[] = []; + for (const mor of props.paths) { + const segs = describePath(m, mor); + if (!segs) { + continue; + } + const idOb = identityPathObject(mor); + const name = + idOb !== null + ? identityText(m, idOb) + : formatPathName(segs.morphisms.map((s) => s.label || "Unnamed")); + out.push({ + mor, + name, + segments: segs, + isIdentity: idOb !== null, + nameLower: normalizePathName(name), + }); + } + return out; + }); + + // Re-association: while the input is not active, react to changes in + // the available entries (e.g. a morphism was renamed, added, removed, + // or the RHS dom/cod filter changed). + // + // Two directions, run in priority order: + // 1. If a committed path no longer appears in the entries + // demote it to unresolved text so the user can see and edit what + // used to be selected. + // 2. Otherwise, if there is unresolved text and it now matches an + // available entry, commit the path and clear the unresolved text. + createEffect(() => { + if (props.focus.hasFocus()) { + return; + } + if (!props.model) { + return; + } + const es = entries(); + const mor = props.mor; + if (mor !== null && !es.some((e) => deepEqual(e.mor, mor))) { + setUnresolvedText(pathText(props.model, mor)); + props.setMor(null); + return; + } + const typed = unresolvedText(); + if (typed === null) { + return; + } + const resolved = resolveTypedPath(typed, es); + if (resolved) { + props.setMor(resolved); + setUnresolvedText(null); + } + }); + + return ( +
    { + // Activate the picker when clicking anywhere inside the + // border, but only when not already in editing mode (so + // selecting text in the input still works). + if (!props.focus.hasFocus()) { + props.focus.setFocused(true); + evt.preventDefault(); + } + }} + > + + } + > + + +
    + ); +} + +/** Inactive view of a path picker: shows the chosen path, last unresolved + typing, or a placeholder. */ +function PathPickerDisplay(props: { + model: DblModel | undefined; + theory: Theory; + mor: Mor | null; + unresolvedText: string | null; +}) { + return ( +
    + ...}> + {(mor) => ( + + )} + + } + > + {(typed) => {typed()}} + +
    + ); +} + +/** Active view of a path picker: an `InlineInput` with a custom completions + list. Fresh-mounted on every activation, so it can own its `text` signal + without any external sync. */ +function PathPickerInput( + props: PathPickerProps & { + entries: PathEntry[]; + initialText: string; + setUnresolvedText: (s: string | null) => void; + }, +) { + const [text, setText] = createSignal(props.initialText); + + /** Wrap each entry into a `Completion` by attaching the `onComplete` + closure that needs access to `setText` and the unresolved-text + setter. Other resolution and rendering data passes through + unchanged on the `path` field. */ + const items = createMemo(() => + props.entries.map((entry) => ({ + name: entry.name, + onComplete: () => { + props.setUnresolvedText(null); + setText(entry.name); + props.setMor(entry.mor); + }, + mor: entry.mor, + path: { + segments: entry.segments, + isIdentity: entry.isIdentity, + nameLower: entry.nameLower, + }, + })), + ); + + const commitTypedText = () => { + const typed = text(); + if (typed.trim() === "") { + props.setUnresolvedText(null); + props.setMor(null); + return; + } + const resolved = resolveTypedPath(typed, props.entries); + if (resolved) { + props.setUnresolvedText(null); + props.setMor(resolved); + return; + } + props.setMor(null); + props.setUnresolvedText(typed); + }; + + const status = () => { + const t = text(); + if (t.trim() === "") { + return null; + } + return resolveTypedPath(t, props.entries) !== null ? null : "incomplete"; + }; + + const hasContent = () => text() !== "" || props.mor !== null; + + return ( + <> + + text={text()} + setText={setText} + placeholder="..." + status={status()} + completions={items()} + completionsFilter={filterPathCompletions} + completionsRenderItem={(item) => ( + + )} + showCompletionsOnFocus={true} + popupClass={styles.completionsPopup} + popoverPlacement="bottom-start" + popoverFloatingOptions={{ flip: false, offset: 8 }} + completionsEmptyText="No matching paths found." + focus={props.focus} + hasBlurred={commitTypedText} + createBelow={props.createBelow} + exitBackward={props.exitBackward} + exitForward={props.exitForward} + exitUp={props.exitUp} + exitDown={props.exitDown} + exitLeft={props.exitLeft} + exitRight={props.exitRight} + /> + +
    + { + // Don't blur the input before clearing. + evt.preventDefault(); + evt.stopPropagation(); + setText(""); + props.setUnresolvedText(null); + props.setMor(null); + }} + > + + +
    +     + + ); +} + +function resolveTypedPath(typed: string, entries: PathEntry[]): Mor | null { + const query = normalizePathName(typed); + if (query === "") { + return null; + } + return entries.find((entry) => entry.nameLower === query)?.mor ?? null; +} + +/** Resolution-relevant data for one path: enough to build a completion row, + filter completions, and resolve typed text. Owned by `PathPicker` so the + parent can re-resolve unresolved text whenever entries change, even + while the input is unmounted. */ +type PathEntry = { + mor: Mor; + name: string; + segments: PathSegments; + isIdentity: boolean; + nameLower: string; +}; + +/** A path completion item. + +Extends `Completion` (so the standard fields like `name` and `onComplete` +are available) and carries an extra `path` field with the data the custom +filter and renderer need (segments for rendering, lower-cased name for +matching). Threaded through `InlineInput`'s generic +parameter so the custom callbacks see the full item type without casts. + */ +type PathCompletionItem = Completion & { + mor: Mor; + path: { + segments: PathSegments; + isIdentity: boolean; + nameLower: string; + }; +}; + +/** Filter path completions, preserving input order (which is already sorted + by edge count upstream in `allPaths`). + +Filtering rules (case-insensitive): +- Empty input matches everything. +- `id`, `id(`, or `id(Foo)` matches every path (identity or otherwise) whose + domain object's label starts with the prefix after the opening parenthesis. + An empty prefix matches all paths. The identity at `Foo` is included + because its domain object is `Foo`. +- `;`-separated tokens match composite paths whose successive morphism + labels start with the corresponding tokens (an empty trailing token is + ignored, so `f;` still matches paths starting with `f`). +- Otherwise, match against the synthesized name (startsWith → includes) or + the path's domain-object label (so e.g. typing `obj` matches `id(object)` + as well as any non-identity path starting at `object`). + */ +function filterPathCompletions(items: PathCompletionItem[], text: string): PathCompletionItem[] { + const trimmed = text.trim(); + if (trimmed === "") { + return items.slice(); + } + const lower = trimmed.toLowerCase(); + const lowerNormalized = normalizePathName(trimmed); + + // Domain-prefixed syntax: `id`, `id(`, `id(Foo`, `id(Foo)`. Matches any + // path whose domain label starts with the prefix (including the + // identity at that object, since its domain is the object). + const idMatch = lower.match(/^id(?:\((.*?)\)?)?$/); + if (idMatch !== null) { + const innerPrefix = idMatch[1] ?? ""; + return items.filter((it) => { + const label = (it.path.segments.dom.label || "Unnamed").toLowerCase(); + return innerPrefix === "" || label.startsWith(innerPrefix); + }); + } + + // Composite-path syntax: `;`-separated label prefixes. + if (lower.includes(";")) { + const tokens = lower.split(";").map((t) => t.trim()); + // Drop a single trailing empty token so `f;` matches paths starting + // with `f`. Other empty tokens (e.g. `f;;g`) prevent any match. + if (tokens.length > 0 && tokens[tokens.length - 1] === "") { + tokens.pop(); + } + if (tokens.some((t) => t === "")) { + return []; + } + return items.filter((it) => { + if (it.path.isIdentity) { + return false; + } + if (it.path.segments.morphisms.length < tokens.length) { + return false; + } + return tokens.every((tok, i) => { + const seg = it.path.segments.morphisms[i]; + invariant(seg, "tokens.length is bounded by morphisms.length"); + const label = (seg.label || "Unnamed").toLowerCase(); + return label.startsWith(tok); + }); + }); + } + + // Fallback: match against the synthesized name or the domain-object + // label. Domain-label matches let typing an object name surface every + // path starting at that object (including its identity). + const starts = items.filter( + (it) => it.path.nameLower.startsWith(lowerNormalized) || domLabel(it).startsWith(lower), + ); + const startsSet = new Set(starts); + const includes = items.filter( + (it) => + !startsSet.has(it) && + (it.path.nameLower.includes(lowerNormalized) || domLabel(it).includes(lower)), + ); + return starts.concat(includes); +} + +function domLabel(it: PathCompletionItem): string { + return (it.path.segments.dom.label || "Unnamed").toLowerCase(); +} + +/** Render a path completion as a single row in the completions list: + typeable name on top as a small caption, diagrammatic path beneath. */ +function PathCompletionRow(props: { item: PathCompletionItem; theory: Theory }) { + return ( +
    +
    + {props.item.name} +
    + +
    + ); +} + +/** Typeable text for an identity path at the given object: `id(Label)`. */ +function identityText(model: DblModel, ob: Ob): string { + const id = basicObId(ob); + const label = id !== null ? labelToString(model.obGeneratorLabel(id)) : ""; + return `id(${label || "Unnamed"})`; +} + +/** Render a simple path diagrammatically. + +Uses the same arrow styling as `MorphismCellEditor`: a leading domain object, +followed by each segment rendered as `[name above arrow] [cod object]`, with +arrow style and object/morphism classes coming from theory metadata. Identity +paths produce no segments, so they render as the styled object node alone. + */ +function PathView(props: { model: DblModel | undefined; theory: Theory; mor: Mor }) { + const segments = createMemo(() => describePath(props.model, props.mor)); + + return ( + (invalid path)}> + {(segs) => } + + ); +} + +/** Maximum number of morphism segments to render before abbreviating with + a mid-path ellipsis. Paths longer than this collapse to the first + `ABBREV_HEAD` and last `ABBREV_TAIL` segments with `...` between. */ +const ABBREV_THRESHOLD = 6; +const ABBREV_HEAD = 3; +const ABBREV_TAIL = 3; + +/** Items rendered between the leading domain object and any further + segments. Either an (arrow + cod) segment, a mid-path ellipsis, or a + "resume" object node rendered after the ellipsis so the first tail + segment (which itself only carries an arrow + cod) is anchored at a + visible domain object. */ +type PathSegmentItem = + | { kind: "segment"; segment: PathMorSegment } + | { kind: "ellipsis" } + | { kind: "object"; ob: PathObSegment }; + +function abbreviateSegments(morphisms: PathMorSegment[]): PathSegmentItem[] { + if (morphisms.length <= ABBREV_THRESHOLD) { + return morphisms.map((segment) => ({ kind: "segment", segment })); + } + const head = morphisms.slice(0, ABBREV_HEAD); + const tail = morphisms.slice(morphisms.length - ABBREV_TAIL); + // Domain of the first tail segment: equals the cod of + // `morphisms[morphisms.length - ABBREV_TAIL - 1]`. Render it after the + // ellipsis so the tail's first arrow has a visible source object. + const firstTailDomIdx = morphisms.length - ABBREV_TAIL - 1; + const resumeOb = morphisms[firstTailDomIdx]?.cod; + const items: PathSegmentItem[] = head.map( + (segment): PathSegmentItem => ({ kind: "segment", segment }), + ); + items.push({ kind: "ellipsis" }); + if (resumeOb) { + items.push({ kind: "object", ob: resumeOb }); + } + items.push(...tail.map((segment): PathSegmentItem => ({ kind: "segment", segment }))); + return items; +} + +function PathSegmentsView(props: { segments: PathSegments; theory: Theory }) { + const domClasses = () => [styles.object, ...obClasses(props.theory, props.segments.dom.obType)]; + const items = createMemo(() => abbreviateSegments(props.segments.morphisms)); + return ( +
    +
    + +
    + + {(item) => { + if (item.kind === "segment") { + return ; + } + if (item.kind === "object") { + const obNodeClasses = [ + styles.object, + ...obClasses(props.theory, item.ob.obType), + ]; + return ( +
    + +
    + ); + } + return ( + + ); + }} +     +
    + ); +} + +/** Render a single (morphism, codomain) segment of a path. + +Mirrors the layout of `MorphismCellEditor`: the morphism name sits above an +arrow drawn in the theory's arrow style; the codomain is rendered with the +object type's CSS classes. + */ +function PathSegmentView(props: { segment: PathMorSegment; theory: Theory }) { + const morTypeMeta = () => + props.segment.morType ? props.theory.modelMorTypeMeta(props.segment.morType) : undefined; + + const arrowClass = () => arrowStyles[morTypeMeta()?.arrowStyle ?? "default"]; + + const nameClasses = () => [ + styles.morName, + arrowStyles.arrowName, + ...(morTypeMeta()?.textClasses ?? []), + ]; + + const codClasses = () => [styles.object, ...obClasses(props.theory, props.segment.cod.obType)]; + + return ( +
    +
    +
    + +
    +
    +
    +
    +
    +
    + +
    +
    + ); +} + +/** Render a label, falling back to a styled "Unnamed" when empty. */ +function LabelOrUnnamed(props: { name: string }) { + return ( + Unnamed}> + {props.name} + + ); +} + +/** A single segment of a path: a morphism plus its codomain. */ +type PathMorSegment = { + label: string; + morType: MorType | undefined; + cod: PathObSegment; +}; + +/** An object as displayed in a path. */ +type PathObSegment = { + label: string; + obType: ObType | undefined; +}; + +type PathSegments = { + /** The path's domain (initial object). */ + dom: PathObSegment; + /** N segments for a path of N morphisms. */ + morphisms: PathMorSegment[]; +}; + +/** Compute display data for the segments making up a path. + +Returns null if the morphism cannot be presented (e.g., contains +non-basic morphisms). + */ +function describePath(model: DblModel | undefined, mor: Mor): PathSegments | null { + if (!model) { + return null; + } + + // Identity path: Mor::Composite(Path::Id(ob)). Display as just the object, + // matching the leading-domain-object rendering of a regular path. + const idOb = identityPathObject(mor); + if (idOb !== null) { + return { dom: describeObSegment(model, idOb), morphisms: [] }; + } + + // Single-morphism path written as Mor::Basic(uuid). + const basicId = match(mor) + .with({ tag: "Basic", content: P.select() }, (id) => id) + .otherwise(() => null); + if (basicId !== null) { + const seg = describeMorSegment(model, basicId); + if (!seg) { + return null; + } + const dom = morDom(model, mor); + return { dom: describeObSegment(model, dom), morphisms: [seg] }; + } + + // Composite sequence: Mor::Composite(Path::Seq([Mor::Basic, ...])). + const seq = match(mor) + .with( + { + tag: "Composite", + content: { tag: "Seq", content: P.select() }, + }, + (xs) => xs, + ) + .otherwise(() => null); + if (seq === null || seq.length === 0) { + return null; + } + const morphisms: PathMorSegment[] = []; + for (const m of seq) { + const id = match(m) + .with({ tag: "Basic", content: P.select() }, (id) => id) + .otherwise(() => null); + if (id === null) { + return null; + } + const seg = describeMorSegment(model, id); + if (!seg) { + return null; + } + morphisms.push(seg); + } + const dom = morDom(model, mor); + return { dom: describeObSegment(model, dom), morphisms }; +} + +function describeMorSegment(model: DblModel, id: string): PathMorSegment | null { + const pres = model.morPresentation(id); + if (!pres) { + return null; + } + return { + label: labelToString(model.morGeneratorLabel(id)), + morType: pres.morType, + cod: describeObSegment(model, pres.cod), + }; +} + +function describeObSegment(model: DblModel, ob: Ob | null): PathObSegment { + if (ob === null) { + return { label: "", obType: undefined }; + } + const id = basicObId(ob); + let obType: ObType | undefined; + try { + obType = model.obType(ob); + } catch { + obType = undefined; + } + return { + label: id !== null ? labelToString(model.obGeneratorLabel(id)) : "", + obType, + }; +} + +/** Render a qualified label as a dotted string, or "" if no label is set. + +The `""` case is handled by the consumer (typically rendered as a styled +"Unnamed" placeholder). + */ +function labelToString(label: QualifiedLabel | undefined): string { + if (!label || label.length === 0) { + return ""; + } + return label.map((seg) => (typeof seg === "string" ? seg : String(seg))).join("."); +} diff --git a/packages/frontend/src/model/model_editor.tsx b/packages/frontend/src/model/model_editor.tsx index 8236b2e21..5673d4832 100644 --- a/packages/frontend/src/model/model_editor.tsx +++ b/packages/frontend/src/model/model_editor.tsx @@ -3,12 +3,19 @@ import { Dynamic } from "solid-js/web"; import invariant from "tiny-invariant"; import { Model, Nb } from "catcolab-document-methods"; -import type { InstantiatedModel, ModelJudgment, MorDecl, ObDecl } from "catcolab-document-types"; +import type { + EqnDecl, + InstantiatedModel, + ModelJudgment, + MorDecl, + ObDecl, +} from "catcolab-document-types"; import { type FocusHandle } from "catcolab-ui-components"; import { type CellConstructor, type FormalCellEditorProps, NotebookEditor } from "../notebook"; import { TheoryLibraryContext, type ModelTypeMeta, type Theory } from "../theory"; import { LiveModelContext } from "./context"; import type { LiveModelDoc } from "./document"; +import EquationCellEditor from "./equation_cell_editor"; import { InstantiationCellEditor } from "./instantiation_cell_editor"; /** Notebook editor for a model of a double theory. @@ -104,6 +111,19 @@ export function ModelCellEditor(props: FormalCellEditorProps) { actions={props.actions} /> + + {(theory) => ( + + props.changeContent((content) => f(content as EqnDecl)) + } + focus={props.focus} + actions={props.actions} + theory={theory()} + /> + )} + ); } @@ -121,6 +141,17 @@ function modelCellConstructors(theory: Theory): CellConstructor[] for (const meta of theory.modelTypes ?? []) { constructors.push(modelCellConstructor(meta)); } + const eqMeta = theory.equationCellMeta; + if (eqMeta) { + constructors.push({ + name: eqMeta.name, + description: eqMeta.description, + shortcut: eqMeta.shortcut, + construct() { + return Nb.newFormalCell(Model.newEquationDecl()); + }, + }); + } return constructors; } @@ -156,7 +187,7 @@ function judgmentLabel(judgment: ModelJudgment): string | undefined { case "instantiation": return theory?.name; case "equation": - return "Equation"; + return theory?.equationCellMeta?.name ?? "Equation"; default: judgment satisfies never; } diff --git a/packages/frontend/src/stdlib/theories/simple-olog.ts b/packages/frontend/src/stdlib/theories/simple-olog.ts index e8eae2a28..83caacb54 100644 --- a/packages/frontend/src/stdlib/theories/simple-olog.ts +++ b/packages/frontend/src/stdlib/theories/simple-olog.ts @@ -16,6 +16,11 @@ export default function createOlogTheory(theoryMeta: TheoryMeta): Theory { return new Theory({ ...theoryMeta, theory: thCategory.theory(), + equationCellMeta: { + name: "Fact", + description: "Add a fact relating aspects", + shortcut: ["F"], + }, pushforwards: [ { target: "simple-schema", diff --git a/packages/frontend/src/stdlib/theories/simple-schema.ts b/packages/frontend/src/stdlib/theories/simple-schema.ts index 67b38a570..1184aef6e 100644 --- a/packages/frontend/src/stdlib/theories/simple-schema.ts +++ b/packages/frontend/src/stdlib/theories/simple-schema.ts @@ -30,6 +30,11 @@ export default function createSchemaTheory(theoryMeta: TheoryMeta): Theory { return new Theory({ ...theoryMeta, theory: thSchema.theory(), + equationCellMeta: { + name: "Equation", + description: "Add an equation between morphisms", + shortcut: ["E"], + }, pushforwards: [ { target: "simple-olog", diff --git a/packages/frontend/src/theory/theory.ts b/packages/frontend/src/theory/theory.ts index d46c29505..77ac2b801 100644 --- a/packages/frontend/src/theory/theory.ts +++ b/packages/frontend/src/theory/theory.ts @@ -79,6 +79,15 @@ export class Theory { /** Whether models of the double theory are constrained to be free. */ readonly onlyFreeModels!: boolean; + /** Metadata for equation cells in the model editor. + + When defined, equation cells are supported in models of this theory and + these labels drive the cell-add menu and the cell label badge. Equation + cells rely on `listSimplePaths`, which only works on discrete double + models, so theories that opt in must have discrete models. + */ + readonly equationCellMeta?: EquationCellMeta; + /** Human-readable name for instances of models of theory. Defaults to "Instance of". @@ -130,6 +139,7 @@ export class Theory { modelTypes?: ModelTypeMeta[]; modelAnalyses?: ModelAnalysisMeta[]; onlyFreeModels?: boolean; + equationCellMeta?: EquationCellMeta; instanceOfName?: string; instanceTypes?: InstanceTypeMeta[]; diagramAnalyses?: DiagramAnalysisMeta[]; @@ -162,6 +172,7 @@ export class Theory { } this.modelAnalysisMap = uniqueIndexArray(props.modelAnalyses ?? [], (meta) => meta.id); this.onlyFreeModels = props.onlyFreeModels ?? false; + this.equationCellMeta = props.equationCellMeta; // Instances. this.instanceOfName = props.instanceOfName ?? "Instance of"; @@ -184,6 +195,11 @@ export class Theory { return this.inclusions.concat(this.pushforwards.map((m) => m.target)); } + /** Whether equation cells are supported in the model editor. */ + get supportsEquations(): boolean { + return this.equationCellMeta !== undefined; + } + /** Get metadata for an object type as used in models. */ modelObTypeMeta(typ: ObType): ModelObTypeMeta | undefined { return this.modelObTypeMap.get(typ); @@ -239,6 +255,18 @@ export class Theory { } } +/** Metadata for equation cells in a model editor. */ +export type EquationCellMeta = { + /** Human-readable name shown in the cell-add menu and as the cell label. */ + name: string; + + /** Tooltip-length description for the cell-add menu. */ + description: string; + + /** Keyboard shortcut for the cell-add menu. */ + shortcut: KbdKey[]; +}; + /** Frontend metadata applicable to any type in a double theory. */ export type BaseTypeMeta = { /** Human-readable name of type. */ diff --git a/packages/ui-components/src/completions.stories.tsx b/packages/ui-components/src/completions.stories.tsx index 98fefcd6c..0cec5e0d4 100644 --- a/packages/ui-components/src/completions.stories.tsx +++ b/packages/ui-components/src/completions.stories.tsx @@ -162,3 +162,65 @@ export const CustomEmptyText: Story = { return ; }, }; + +type ColoredItem = { + name: string; + tags: string[]; + color: string; +}; + +const COLORED_ITEMS: ColoredItem[] = [ + { name: "Apple", tags: ["fruit", "red"], color: "#e23" }, + { name: "Avocado", tags: ["fruit", "green"], color: "#5a3" }, + { name: "Banana", tags: ["fruit", "yellow"], color: "#dc4" }, + { name: "Carrot", tags: ["vegetable", "orange"], color: "#e72" }, + { name: "Cabbage", tags: ["vegetable", "green"], color: "#7a5" }, +]; + +// Custom filter: match if any tag starts with the input, or the name +// contains it. +const filterColoredItems = (xs: ColoredItem[], q: string) => { + const lower = q.toLowerCase(); + return xs.filter( + (it) => it.name.toLowerCase().includes(lower) || it.tags.some((t) => t.startsWith(lower)), + ); +}; + +const renderColoredItem = (item: ColoredItem) => ( +
    +
    + {item.name} + {item.tags.join(", ")} +
    +); + +export const CustomFilterAndRenderer: Story = { + render: () => { + const [text, setText] = createSignal(""); + return ( +
    + setText(e.currentTarget.value)} + placeholder="Try `fruit`, `green`, `app`..." + style={{ "margin-bottom": "8px", padding: "4px", width: "260px" }} + /> + + completions={COLORED_ITEMS} + text={text()} + filter={filterColoredItems} + renderItem={renderColoredItem} + onSelect={(it) => alert(`Selected ${it.name}`)} + /> +
    + ); + }, +}; diff --git a/packages/ui-components/src/completions.tsx b/packages/ui-components/src/completions.tsx index 824737a99..f8a7737a7 100644 --- a/packages/ui-components/src/completions.tsx +++ b/packages/ui-components/src/completions.tsx @@ -25,8 +25,9 @@ export type Completion = { onComplete?: () => void; }; -export type CompletionsRef = { - remainingCompletions: () => Completion[]; +/** Imperative handle for a `Completions` component. */ +export type CompletionsRef = { + remainingCompletions: () => T[]; presumptive: () => number; setPresumptive: (i: number) => void; previousPresumptive: () => void; @@ -34,42 +35,120 @@ export type CompletionsRef = { selectPresumptive: () => void; }; -export function Completions(props: { - completions: Completion[]; +/** Default filter for `Completion`-shaped items. + +Returns items whose `name` starts with the input text first, followed by +items whose `name` contains it (case-insensitive). Items already matched in +the first pass are not duplicated in the second. + +Generic in `T extends Completion`: the body only reads the `name` field, so +the input element type is preserved through the filter. + */ +export function defaultCompletionFilter(items: T[], text: string): T[] { + const prefix = text.toLowerCase(); + const starts = items.filter((c) => c.name.toLowerCase().startsWith(prefix)); + const startsNames = new Set(starts.map((c) => c.name.toLowerCase())); + const includes = items.filter( + (c) => c.name.toLowerCase().includes(prefix) && !startsNames.has(c.name.toLowerCase()), + ); + return starts.concat(includes); +} + +/** Default item renderer for `Completion`-shaped items. */ +export function defaultCompletionRenderer(item: Completion): JSX.Element { + return ( + <> +
    + +
    {item.icon}
    +     +
    {item.name}
    + +
    + +
    +     +
    + +
    {item.description}
    +     + + ); +} + +/** Default selection handler for `Completion`-shaped items. */ +export function defaultCompletionOnSelect(item: Completion): void { + item.onComplete?.(); +} + +/** Props for the `Completions` component. + +Generic in the item type `T`, constrained to extend `Completion` so the +built-in defaults remain applicable. The `filter`, `renderItem`, and +`onSelect` callbacks are optional; when omitted, the corresponding +`defaultCompletion*` helper is used. + */ +export type CompletionsProps = { + /** Raw list of items. The displayed list is `filter(items, text ?? "")`. */ + completions: T[]; + + /** Current input text used for filtering. */ text?: string; + + /** Text shown when no completions match. Defaults to "No completions". */ emptyText?: string; + + /** Called after an item has been selected. Fires after `onSelect`. */ onComplete?: () => void; - ref?: (ref: CompletionsRef) => void; -}) { + + /** Imperative ref. */ + ref?: (ref: CompletionsRef) => void; + + /** Filter for the completions list. + + Receives the raw list and the current input text; returns the items to + display, in display order. Defaults to `defaultCompletionFilter`. + */ + filter?: (items: T[], text: string) => T[]; + + /** Renderer for an item. Defaults to `defaultCompletionRenderer`. */ + renderItem?: (item: T, presumptive: boolean) => JSX.Element; + + /** Called when an item is selected. Defaults to + `defaultCompletionOnSelect`. */ + onSelect?: (item: T) => void; +}; + +/** Completions list. + +Renders a filterable, keyboard-navigable list of items, generic in the +item type `T extends Completion`. The `filter`, `renderItem`, and +`onSelect` callbacks fall back to the built-in `defaultCompletion*` +helpers when not supplied. + */ +export function Completions(props: CompletionsProps) { const [presumptive, setPresumptive] = createSignal(0); const previousPresumptive = () => setPresumptive((i) => Math.max(0, i - 1)); const nextPresumptive = () => setPresumptive((i) => Math.min(remainingCompletions().length - 1, i + 1)); - const remainingCompletions = createMemo(() => { + const remainingCompletions = createMemo(() => { setPresumptive(0); - const prefix = props.text?.toLowerCase() ?? ""; - const starts = props.completions?.filter((c) => c.name.toLowerCase().startsWith(prefix)); - const startsNames = new Set(starts.map((c) => c.name.toLowerCase())); - const includes = - props.completions?.filter( - (c) => - c.name.toLowerCase().includes(prefix) && !startsNames.has(c.name.toLowerCase()), - ) ?? []; - return starts.concat(includes); + const filter = props.filter ?? defaultCompletionFilter; + return filter(props.completions, props.text ?? ""); }); - const selectPresumptive = () => { - const completion = remainingCompletions()[presumptive()]; - if (completion) { - select(completion); - } + const select = (item: T) => { + (props.onSelect ?? defaultCompletionOnSelect)(item); + props.onComplete?.(); }; - const select = (completion: Completion) => { - completion.onComplete?.(); - props.onComplete?.(); + const selectPresumptive = () => { + const item = remainingCompletions()[presumptive()]; + if (item !== undefined) { + select(item); + } }; onMount(() => @@ -98,20 +177,7 @@ export function Completions(props: { onMouseOver={() => setPresumptive(i())} onMouseDown={() => select(c)} > -
    - -
    {c.icon}
    -     -
    {c.name}
    - -
    - -
    -     -
    - -
    {c.description}
    -     + {(props.renderItem ?? defaultCompletionRenderer)(c, i() === presumptive())}
    • )} diff --git a/packages/ui-components/src/inline_input.tsx b/packages/ui-components/src/inline_input.tsx index 9e584270f..3e0c70d3a 100644 --- a/packages/ui-components/src/inline_input.tsx +++ b/packages/ui-components/src/inline_input.tsx @@ -1,15 +1,16 @@ +import type { Completion } from "./completions"; import { TextInput, type TextInputOptions } from "./text_input"; import "./inline_input.css"; /** Props for `InlineInput` component */ -type InlineInputProps = InlineInputOptions & { +type InlineInputProps = InlineInputOptions & { text: string; setText: (text: string) => void; }; /** Optional props for `InlineInput` component. */ -export type InlineInputOptions = TextInputOptions & { +export type InlineInputOptions = TextInputOptions & { placeholder?: string; status?: InlineInputErrorStatus; }; @@ -22,13 +23,16 @@ export type InlineInputErrorStatus = null | "incomplete" | "invalid"; Unlike a typical `input` element, this component resizes itself to fit its content, instead of having a fixed width. It is styled to blend into surrounding content, e.g., it has no border or background. + +Generic in the completion item type `T`, forwarded to `TextInput`. Defaults +to `T = Completion`. */ -export const InlineInput = (props: InlineInputProps) => ( +export const InlineInput = (props: InlineInputProps) => ( // Uses a hidden filler element to size the input field: // https://stackoverflow.com/a/41389961
    {props.text || props.placeholder} - class="inline-input" classList={{ incomplete: props.status === "incomplete", diff --git a/packages/ui-components/src/text_input.tsx b/packages/ui-components/src/text_input.tsx index c3aeaef2b..b71a9d26a 100644 --- a/packages/ui-components/src/text_input.tsx +++ b/packages/ui-components/src/text_input.tsx @@ -8,18 +8,37 @@ import { type Completion, Completions, type CompletionsRef } from "./completions import type { FocusHandle } from "./util/focus"; import { assertTypelevel } from "./util/types"; +/** Floating-options type accepted by Corvu's `Popover`. */ +export type PopoverFloatingOptions = NonNullable< + NonNullable["floatingOptions"]> +>; + +/** Custom filter for completions in `TextInput`. */ +export type TextInputCompletionFilter = (items: T[], text: string) => T[]; + +/** Custom item renderer for completions in `TextInput`. */ +export type TextInputCompletionRenderer = ( + item: T, + presumptive: boolean, +) => JSX.Element; + +/** Custom selection handler for completions in `TextInput`. */ +export type TextInputCompletionOnSelect = (item: T) => void; + /** Props for `TextInput` component. */ -type TextInputProps = Omit, "onKeyDown"> & - TextInputOptions & { +type TextInputProps = Omit< + ComponentProps<"input">, + "onKeyDown" +> & + TextInputOptions & { text: string; setText: (text: string) => void; }; /** Optional props available to a `TextInput` component. */ -export type TextInputOptions = TextInputActions & { +export type TextInputOptions = TextInputActions & { /** Focus state for this input. */ focus?: FocusHandle; - /** Whether the input is active: allowed to the grab the focus. */ isActive?: boolean; @@ -30,7 +49,7 @@ export type TextInputOptions = TextInputActions & { hasBlurred?: () => void; /** List of possible auto-completions. */ - completions?: Completion[]; + completions?: T[]; /** Whether to show possible auto-completions when focus is gained. Defaults to yes. */ showCompletionsOnFocus?: boolean; @@ -41,6 +60,31 @@ export type TextInputOptions = TextInputActions & { /** Text shown when no completions match. Defaults to "No completions". */ completionsEmptyText?: string; + /** Custom filter for the completions list. + + Defaults to a built-in startsWith → includes match against + `Completion.name`. + */ + completionsFilter?: TextInputCompletionFilter; + + /** Custom renderer for completion items. + + Defaults to the built-in icon/name/shortcut/description layout. + */ + completionsRenderItem?: TextInputCompletionRenderer; + + /** Custom selection handler for completions. + + Defaults to invoking `Completion.onComplete`. + */ + completionsOnSelect?: TextInputCompletionOnSelect; + + /** Placement of the completions popup. Defaults to `"bottom-start"`. */ + popoverPlacement?: ComponentProps["placement"]; + + /** Floating-UI options forwarded to Corvu's `Popover`. */ + popoverFloatingOptions?: PopoverFloatingOptions; + /** Called to intercept `keydown` events.` Return `true` to intercept the event and prevent normal processing. @@ -115,6 +159,11 @@ const TEXT_INPUT_OPTIONS = [ "showCompletionsOnFocus", "popupClass", "completionsEmptyText", + "completionsFilter", + "completionsRenderItem", + "completionsOnSelect", + "popoverPlacement", + "popoverFloatingOptions", "interceptKeyDown", "autofill", "createBelow", @@ -137,8 +186,13 @@ void assertTypelevel< The input field itself is just an unstyled `` element. A host of options are provided for managing focus of this and nearby components, as well as showing auto-completions. + +Generic in the completion item type `T`, which must extend `Completion` so +that the built-in defaults for `completionsFilter`, `completionsRenderItem`, +and `completionsOnSelect` (which only read `Completion` fields) remain +valid. Defaults to `T = Completion`. */ -export function TextInput(allProps: TextInputProps) { +export function TextInput(allProps: TextInputProps) { const [props, options, inputProps] = splitProps( allProps, ["text", "setText"], @@ -156,7 +210,7 @@ export function TextInput(allProps: TextInputProps) { }); const [isCompletionsOpen, setCompletionsOpen] = createSignal(false); - const [completionsRef, setCompletionsRef] = createSignal(); + const [completionsRef, setCompletionsRef] = createSignal>(); const onKeyDown: JSX.EventHandler = (evt) => { const remaining = completionsRef()?.remainingCompletions() ?? []; @@ -220,7 +274,8 @@ export function TextInput(allProps: TextInputProps) { completionsRef()?.setPresumptive(0); } }} - placement="bottom-start" + placement={options.popoverPlacement ?? "bottom-start"} + floatingOptions={options.popoverFloatingOptions} closeOnOutsideFocus={false} closeOnOutsidePointer={false} trapFocus={false} @@ -257,10 +312,13 @@ export function TextInput(allProps: TextInputProps) { - completions={options.completions ?? []} text={props.text} emptyText={options.completionsEmptyText} + filter={options.completionsFilter} + renderItem={options.completionsRenderItem} + onSelect={options.completionsOnSelect} ref={setCompletionsRef} onComplete={() => setCompletionsOpen(false)} /> From fb4740f08c69fa5240818d50b75415c9d4814670 Mon Sep 17 00:00:00 2001 From: Kaspar Bumke Date: Tue, 12 May 2026 14:16:34 +0100 Subject: [PATCH 4/6] ENH: Reduce spacing in path equations editor --- packages/frontend/src/model/equation_cell_editor.module.css | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/packages/frontend/src/model/equation_cell_editor.module.css b/packages/frontend/src/model/equation_cell_editor.module.css index 6bb2086dd..b4f07d71a 100644 --- a/packages/frontend/src/model/equation_cell_editor.module.css +++ b/packages/frontend/src/model/equation_cell_editor.module.css @@ -10,7 +10,6 @@ .body { display: flex; flex-direction: column; - gap: 0.5em; position: relative; margin-left: 0.5rem; padding-left: 1rem; @@ -39,18 +38,17 @@ align-items: center; justify-content: center; gap: 1ex; - width: 100%; min-width: 0; box-sizing: border-box; - padding: 0.75em 1em; + padding: 0 1em; cursor: text; - min-height: 90px; } .equals { font-size: 1.5em; text-align: center; line-height: 1; + padding-bottom: 0.5em; } .pathDisplay { From e7fb4a30e4573e8d5d6a033b1faebee1319851e2 Mon Sep 17 00:00:00 2001 From: Kaspar Bumke Date: Tue, 12 May 2026 15:26:58 +0100 Subject: [PATCH 5/6] ENH: Use ghost path equation editor to avoid layout shift --- .../src/model/equation_cell_editor.module.css | 41 +++++++++++++-- .../src/model/equation_cell_editor.tsx | 50 ++++++++++++------- 2 files changed, 69 insertions(+), 22 deletions(-) diff --git a/packages/frontend/src/model/equation_cell_editor.module.css b/packages/frontend/src/model/equation_cell_editor.module.css index b4f07d71a..e60e47d24 100644 --- a/packages/frontend/src/model/equation_cell_editor.module.css +++ b/packages/frontend/src/model/equation_cell_editor.module.css @@ -33,15 +33,42 @@ } .pathPicker { + /* Single-cell grid so the display (always rendered) and the input + layer (mounted when active) stack on top of each other. The + display drives the cell's intrinsic height — so the row's height + matches the current path's natural rendered height (one line, or + multiple when wrapped) and doesn't shift when toggling into the + input. */ + display: grid; + grid-template-columns: minmax(0, 1fr); + min-width: 0; + box-sizing: border-box; + padding: 0 1em; + cursor: text; +} + +.pathPicker > * { + grid-area: 1 / 1; +} + +/* Hidden-but-laid-out display, used while the input is active so the + picker keeps the display's height. */ +.ghost { + visibility: hidden; + pointer-events: none; +} + +/* Wrapper around the active `InlineInput` (+ clear button). Stacks on top + of the (now-hidden) display via the grid above, and arranges the input + and the trailing clear button on a single row, centred like the + original flex layout. */ +.inputLayer { display: flex; flex-direction: row; align-items: center; justify-content: center; gap: 1ex; min-width: 0; - box-sizing: border-box; - padding: 0 1em; - cursor: text; } .equals { @@ -53,7 +80,13 @@ .pathDisplay { cursor: text; - display: block; + /* Centre fallback content (placeholder/unresolved-text spans) the + way the previous flex-row `.pathPicker` did. `` does + its own centring via the inner `.path` flex container. */ + display: flex; + flex-direction: row; + align-items: center; + justify-content: center; min-width: 0; } diff --git a/packages/frontend/src/model/equation_cell_editor.tsx b/packages/frontend/src/model/equation_cell_editor.tsx index 4a1299fed..60331af26 100644 --- a/packages/frontend/src/model/equation_cell_editor.tsx +++ b/packages/frontend/src/model/equation_cell_editor.tsx @@ -344,38 +344,52 @@ function PathPicker(props: PathPickerProps) { } }} > -
    ); } /** Inactive view of a path picker: shows the chosen path, last unresolved - typing, or a placeholder. */ + typing, or a placeholder. + + When `ghost` is true the display is rendered for layout only — it is + hidden visually and made inert, but still contributes its intrinsic + height to the surrounding picker so the input mode (stacked on top) + doesn't shrink the row. */ function PathPickerDisplay(props: { model: DblModel | undefined; theory: Theory; mor: Mor | null; unresolvedText: string | null; + ghost?: boolean; }) { return ( -
    +
    Date: Tue, 12 May 2026 15:40:56 +0100 Subject: [PATCH 6/6] ENH: Tweak equation editor spacing --- .../src/model/equation_cell_editor.module.css | 18 +++++++++- .../src/model/equation_cell_editor.tsx | 34 ++++++++++--------- 2 files changed, 35 insertions(+), 17 deletions(-) diff --git a/packages/frontend/src/model/equation_cell_editor.module.css b/packages/frontend/src/model/equation_cell_editor.module.css index e60e47d24..a618c1a56 100644 --- a/packages/frontend/src/model/equation_cell_editor.module.css +++ b/packages/frontend/src/model/equation_cell_editor.module.css @@ -94,16 +94,32 @@ display: flex; flex-direction: row; flex-wrap: wrap; - align-items: center; justify-content: center; gap: 1ex; min-width: 0; + min-height: 60px; box-sizing: border-box; /* Vertical room for morphism names above arrows; see arrow_styles.module.css. */ --formal-judgment-font-size: 0.9em; line-height: 1.2; } +/* Per-side alignment of the diagrammatic path so the two sides of the + equation hug the central `=` sign: LHS sits at the bottom of its row + (against the equals sign above? — actually the equals is between + them, so "hug" means LHS bottoms toward the equals, RHS tops toward + the equals). Applied to the inner `.path` since that is the flex + container holding the path items. */ +.lhs .path { + align-items: center; + align-content: center; +} + +.rhs .path { + align-items: flex-start; + align-content: flex-start; +} + /* A single (arrow + cod object) segment, kept together as one wrappable unit so the arrow never lands on a different line than its codomain. */ .segment { diff --git a/packages/frontend/src/model/equation_cell_editor.tsx b/packages/frontend/src/model/equation_cell_editor.tsx index 60331af26..1b9652b3f 100644 --- a/packages/frontend/src/model/equation_cell_editor.tsx +++ b/packages/frontend/src/model/equation_cell_editor.tsx @@ -199,18 +199,15 @@ export default function EquationCellEditor(props: EquationEditorProps) { paths={allPaths()} mor={props.equation.lhs} setMor={setLhs} - isActive={props.isActive && activeInput() === "lhs"} - exitBackward={() => setActiveInput("name")} - exitForward={() => setActiveInput("rhs")} - exitUp={() => setActiveInput("name")} - exitDown={() => setActiveInput("rhs")} - exitLeft={() => setActiveInput("name")} - exitRight={() => setActiveInput("rhs")} - hasFocused={() => { - setActiveInput("lhs"); - props.actions.hasFocused?.(); - }} - createBelow={() => setActiveInput("rhs")} + focus={focus.childFocus("lhs")} + side="lhs" + exitBackward={() => focus.setActiveChild("name")} + exitForward={() => focus.setActiveChild("rhs")} + exitUp={() => focus.setActiveChild("name")} + exitDown={() => focus.setActiveChild("rhs")} + exitLeft={() => focus.setActiveChild("name")} + exitRight={() => focus.setActiveChild("rhs")} + createBelow={() => focus.setActiveChild("rhs")} />
    {"="}
    setActiveInput("lhs")} + focus={focus.childFocus("rhs")} + side="rhs" + exitBackward={() => focus.setActiveChild("lhs")} exitForward={props.actions.activateBelow} exitUp={() => focus.setActiveChild("lhs")} exitDown={props.actions.activateBelow} @@ -239,7 +237,11 @@ type PathPickerProps = { paths: Mor[]; mor: Mor | null; setMor: (mor: Mor | null) => void; - isActive: boolean; + focus: FocusHandle; + /** Which side of the equation this picker represents. Drives the + per-side alignment of the diagrammatic display (LHS bottom-aligned, + RHS top-aligned) so the two sides hug the centre `=` sign. */ + side: "lhs" | "rhs"; exitBackward?: () => void; exitForward?: () => void; exitUp?: () => void; @@ -333,7 +335,7 @@ function PathPicker(props: PathPickerProps) { return (
    { // Activate the picker when clicking anywhere inside the // border, but only when not already in editing mode (so