Change object/morphism types in model notebooks #895
Conversation
quffaro
added
enhancement
quffaro
force-pushed
the
cm/ui-switch-cell-type
branch
from
ed42237 to
afb459e
Compare
quffaro
force-pushed
the
cm/ui-switch-cell-type
branch
from
36283e9 to
6b18588
Compare
quffaro
force-pushed
the
cm/ui-switch-cell-type
branch
from
6b18588 to
c8b4109
Compare
quffaro
force-pushed
the
cm/ui-switch-cell-type
branch
from
c8b4109 to
6d6a83a
Compare
epatters
changed the title
epatters
left a comment
epatters
left a comment
There was a problem hiding this comment.
Thanks Matt for taking this on!
I have one high-level comment about the architecture, reflected in several of the comments below. Rather than using the cell constructor mechanism to construct a whole new cell and then extract its object/morphism type, we should, in each object declaration cell, create a cell switcher by looking up the available object types directly from the theory, and similarly for the morphism declaration cells. No code in the notebook directory should make reference to theories or models.
| } | ||
|
|
||
| function modelCellConstructors(theory: Theory): CellConstructor<ModelJudgment>[] { | ||
| function modelCellConstructors( |
There was a problem hiding this comment.
I don't think it makes sense to implement this feature by changing modelCellConstructors. As the name suggests, "cell constructors" are functions that construct new notebook cells. This is quite different in scoping to mutating existing cells of a given type.
| "tag" in content && | ||
| content.tag === "morphism" | ||
| ); | ||
| }; |
There was a problem hiding this comment.
A hint that this design is off is that notebook editor is not supposed to know anything about theories, models, etc. It's a completely generic component.
Closes #184.