Node styling improvements#997
Merged
Merged
Conversation
georgefst
commented
Jun 29, 2023
| * Note that the backend could in principal tell us this independently of flavors, | ||
| * since it comes down to whether the node ultimately comes from an `Expr`, `Type` or `Kind`. | ||
| */ | ||
| export const isTypeLevel = (flavor: NodeFlavor): "term" | "type" | "kind" => { |
Contributor
Author
There was a problem hiding this comment.
Is there a good name for "type or term or kind"? The existing naming here was just about okay when we weren't considering kinds, but now it's misleading.
Contributor
Author
There was a problem hiding this comment.
@brprice says "sort" - I'll change this (along with the "principle"/"principal" typo I just noticed here).
Contributor
There was a problem hiding this comment.
I would probably use "sort". It is used this way in Pure Type Systems.
Member
|
My Internet is currently brutally bad, so I won't be able to meaningfully review this. So long as it's more or less in line with #987, I'll be OK with it. |
Contributor
Author
There's no difference in functionality, just some minor code changes. I'd merge, but CI is blocked due to some Vault issue. |
The choices of shape are somewhat arbitrary, but there is a little logic to it: types are rectangular because they're in a sense more "rigid", and kinds are drawn as diamonds since each node currently only has a single character. We considered using `clip-path`, instead of rotation, to create the shape for kinds, but this makes drawing borders difficult as they don't follow the path. The usual trick would be to add a dummy background to create a manual border, but this quickly gets messy when we don't want it for the type or term case. Signed-off-by: George Thomas <georgefsthomas@gmail.com>
Well, almost all. We still use black for type annotations due to running out of colours in our existing palette. We try to colour type nodes analogously to corresponding term nodes. This makes more sense now that we use different shapes for terms and types, but it probably requires a little more thought. For example, it may seem odd that we style term `Lam` and type `LAM` differently, since we choose instead to highlight their analogies with `TFun` and `TForall` directly. We should consider refactors to make this sort of change less laborious, though it's hard to say how to abstract colours properly when tailwind discourages concatenating class strings. Signed-off-by: George Thomas <georgefsthomas@gmail.com> Signed-off-by: Drew Hess <src@drewhess.com>
This covers _all_ sorts of application: term-to-term, term-to-type, and type-to-type. We were already using `@` for two different concepts, so we may as well unify all three. And `$` is a weird Haskell-ism that isn't really used elsewhere. We can now easily tell which sort of application is in use by the shape of children. Signed-off-by: George Thomas <georgefsthomas@gmail.com>
These seem redundant, since patterns already look so different to everthing else. We may wish to re-introduce these in beginner mode. Signed-off-by: George Thomas <georgefsthomas@gmail.com>
georgefst
force-pushed
the
georgefst/zurihac-nodes
branch
from
f564ff1 to
01592cb
Compare
Merged
Closed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This is a cleaned-up version of the bulk of #980/#987.
I've fixed up comments and commit messages, and rebased to fold last commit in earlier. I also fixed a bug where edges out of
THolewere invisible - this turned out to be due to a typo (stroke-red-tertiaryy).