Skip to content

Editor variants and a string diagram variant for Petri nets#1180

Merged
epatters merged 7 commits intomainfrom
kb/flexible-editors
Apr 10, 2026
Merged

Editor variants and a string diagram variant for Petri nets#1180
epatters merged 7 commits intomainfrom
kb/flexible-editors

Conversation

@kasbah
Copy link
Copy Markdown
Member

@kasbah kasbah commented Apr 1, 2026

closes #960
closes #955

image

hover:

image

@epatters epatters added enhancement New feature or request frontend TypeScript frontend and Rust-wasm integrations labels Apr 1, 2026
@kasbah kasbah changed the base branch from kb/arabic-arrows to main April 1, 2026 17:59
@kasbah kasbah force-pushed the kb/flexible-editors branch from 51b2c41 to 5d7d615 Compare April 2, 2026 16:13
@kasbah kasbah changed the title Flexible editors for morphisms and objects Editor variants and a Petri net string diagram editor variant Apr 2, 2026
@kasbah kasbah force-pushed the kb/flexible-editors branch from 5d7d615 to ac5b41b Compare April 2, 2026 16:17
@kasbah kasbah force-pushed the kb/flexible-editors branch 7 times, most recently from 216d820 to e1bbeb9 Compare April 7, 2026 15:24
@kasbah kasbah marked this pull request as ready for review April 7, 2026 16:11
@kasbah kasbah force-pushed the kb/flexible-editors branch 3 times, most recently from e331a47 to c523923 Compare April 7, 2026 17:19
@kasbah kasbah requested a review from epatters April 7, 2026 17:38
tim-at-topos added a commit that referenced this pull request Apr 7, 2026
@kasbah kasbah force-pushed the kb/flexible-editors branch 2 times, most recently from c90463c to 9d09b8d Compare April 8, 2026 11:19
@kasbah kasbah force-pushed the kb/flexible-editors branch from e7f494d to 760771f Compare April 8, 2026 18:43
Copy link
Copy Markdown
Member

@epatters epatters left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is great, thanks Kaspar! I like the overall conception for "editor variants," and the string-diagram-style editor variant Petri nets is very cool.

To my questions/comments below I would add that I agree with @tim-at-topos that the editor variants shouldn't appear in the list of logics/theories but should be settable via some other widget in the model notebook. But we don't have to figure that out right now.

Comment thread packages/frontend/src/model/document.ts Outdated
Comment thread packages/frontend/src/model/document.ts Outdated
Comment thread packages/frontend/src/model/model_editor.tsx Outdated
Comment thread packages/frontend/src/model/model_editor.tsx Outdated
return ob;
}
return { tag: "App", content: { op: applyOp, ob } };
}
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These helpers are duplicative with the wrapping/unwrapping performed in src/model/object_input.

Behind this is the more important point that this component would ideally not bake in the assumption about a particular operation being applied (cf. similar comment below), which couples it unnecessarily closely to a particular theory. To be more specific, a Petri net can be viewed as free symmetric monoidal categories (SMCs) or free PROPs (or other things besides), and we might want to reuse this component for such situations. However, if it's not clear what to do, we can defer this to a future PR.

Comment thread packages/frontend/src/model/string_diagram_morphism_cell_editor.tsx Outdated
Comment thread packages/frontend/src/model/string_diagram_morphism_cell_editor.tsx Outdated
Comment thread packages/frontend/src/stdlib/theories/petri-net.ts Outdated
@epatters epatters changed the title Editor variants and a Petri net string diagram editor variant Editor variants and a string diagram variant for Petri nets Apr 9, 2026
@kasbah
Copy link
Copy Markdown
Member Author

kasbah commented Apr 10, 2026

I believe I've addressed all feedback and I've changed this to be behind a settings pane like the analysis settings.

out.mp4

Copy link
Copy Markdown
Member

@epatters epatters left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, looks wonderful!

@epatters epatters merged commit 9d304d9 into main Apr 10, 2026
17 checks passed
@epatters epatters deleted the kb/flexible-editors branch April 10, 2026 18:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature or request frontend TypeScript frontend and Rust-wasm integrations

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Flexible bindings of editors to object/morphism types Editable widget for multiary morphism generators in string diagram style

2 participants