Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Show something on unconnected ports #24

Open
nomeata opened this issue Sep 22, 2015 · 7 comments
Open

Show something on unconnected ports #24

nomeata opened this issue Sep 22, 2015 · 7 comments
Labels
UI

Comments

@nomeata
Copy link
Owner

nomeata commented Sep 22, 2015

I.e. the proposition that would be there if one had a connection with nothing else there.

Could use the same display style as for the prototypes.
@nomeata nomeata added the UI label Sep 24, 2015
@nomeata
Copy link
Owner Author

nomeata commented Sep 24, 2015

Marked as a UI bug, but this will require some adjustments in the logic, i.e. return a map from port description to proposition. When this is done, it might make sense to return only the status of each connection, as the label for the connection can be fetched from map just mentioned.

@gattschardo
Copy link
Collaborator

The port to prop map is something that is also needed for the rule export, see 315f8f8, Analysis.prepare returns the BlockProps map which contains the relevant info.

@nomeata
Copy link
Owner Author

nomeata commented Sep 24, 2015

Nice. Although I would expect type Map PortSpec Proposition there, as assumption and conclusions also need a proposition at their port. OTOH, I consider adding them as blocks as well, in which case PortSpec becomes isomorphic to (Key Block, Key Port), in which case we are almost back at what we have right now. All in all: Either works :-)

@gattschardo
Copy link
Collaborator

assumption and conclusions also need a proposition at their port.

Do they? They have their proposition written on them anyways, so if nothing is connected, there is no extra information to display on their ports, right?

@nomeata
Copy link
Owner Author

nomeata commented Sep 25, 2015

Yes, but the fact that the proposition written on them is, in a way, a deviation from the usual. If I knew what else I could put on there, I’d rather do that :-)

@NicoleRauch
Copy link
Collaborator

Maybe "START" and "GOAL"? But I'd also prefer to directly see the propositions written on them. It's like these blocks are good for providing these propositions, and the other blocks are good for providing some "adaptors" or something. So I don't see a real deviation there.

nomeata added a commit that referenced this issue Sep 26, 2015
@nomeata
Refactor prepare
84384d2 
to return a more polished and selfcontained description of the proof,
with renaming and scopes taken care of. This simplifies later stages
(look, no "task" any more), and also prepares for #24.

I removed one of the test cases; the test suite looks a bit too messy
anyway right now. At least I could not make quick sense of what belongs
to what :-). We should rely more on the tests based on the examples
directory, that is easier to maintain.
nomeata added a commit that referenced this issue Sep 26, 2015
@nomeata
Get rid of LabelConnections
f9c9f5a 
we now return a map from PortSpec to Proposition (more preparation for
bug #24) and a simple enumeration type for the status of each
connection.

This patch is incomplete, as there is no nice way to represent the map
from PortSpec in JSON. So I’ll first refacort PortSpec into a simple
product type, and then work on this can continue.
@nomeata nomeata mentioned this issue Oct 4, 2015
Open
@nomeata
Copy link
Owner Author

nomeata commented May 20, 2016

Also wanted by one of the ITP reviewers.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
UI
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@nomeata @gattschardo @NicoleRauch