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.

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

Infoview DocumentPosition should be a context #197

Closed
EdAyers opened this issue Jun 17, 2022 · 5 comments
Closed

Infoview DocumentPosition should be a context #197

EdAyers opened this issue Jun 17, 2022 · 5 comments

Comments

@EdAyers
Copy link
Contributor

EdAyers commented Jun 17, 2022

Currently in the infoview code, every component is passing the pos : DocumentPosition prop up through the component hierarchy. I think it would make a lot of sense to make this a React context instead.

@gebner
Copy link
Member

gebner commented Jun 17, 2022

I'm not sure if this is such a good idea. We have a lot of different positions floating around.

  1. The cursor position in the editor.
  2. The position of the current info (which may be different from the cursor position if it's pinned).
  3. The position of the data shown in the info (which may lag behind the info position when the cursor is moved).
  4. The position used for RPC queries.
  5. The position of the diagnostic message / term goal / widget.

It goes without saying that all of these can be different. I vaguely recall that we've had some issues mixing up 2 and 3 but I can't find it right now.

@lovettchris
Copy link
Contributor

lovettchris commented Jun 20, 2022

I agree with Gabriel, I think "pinning" shows an example where a react component needs it's own local "pos" that is not in a shared context. You see this in Infos.tsx where the pos being passed down to the component is conditionally coming from the curLoc state or the pinnedPoss state. Infos is also listening to the ec.events.changedCursorLocation event so it can update when the current location is changed. AllMessages is also an example of a React component in the info view that does not use the cursor location at all.

image

I am curious about the naming of pinnedPoss and setPinnedPoss. I would have named these pinnedPos and setPinnedPos. I'm not sure what the second s at the and of those names represents exactly... it's not like it is plural positions or anything... so a bit confusing to me? Or is it plural because of the pinKey.current refcount?

@EdAyers
Copy link
Contributor Author

EdAyers commented Jun 21, 2022

There are different poses flying around but once you are inside the body of InfoDisplay there is only one pos. so the proposal would be to add pos as a context there.

@gebner
Copy link
Member

gebner commented Jun 21, 2022

once you are inside the body of InfoDisplay there is only one pos

Inside of InfoDisplay you still have the positions (2)-(5) from my list.

@EdAyers
Copy link
Contributor Author

EdAyers commented Jun 21, 2022

ok within GoalUI, but also MessageView does its own thing with positions and can ignore the context. Eg the context could be called InfoDisplayPosContext.

I'm going to close because also this doesn't matter.

@EdAyers EdAyers closed this as completed Jun 21, 2022
Vtec234 added a commit that referenced this issue Jun 3, 2024
Implementation of leanprover/lean4#2064.

Besides adding support for widget messages, this adds an `EnvPosContext`
that stores the position that a component is "about" (see the docstring
for more detail). This was originally proposed in #197 and eventually
dismissed (see #226 for a detailed discussion), but I think it warrants
a reconsideration. While Gabriel's point that there are many positions
around remains true, the `EnvPosContext` stores a very specific one.
This position is only used to retrieve a snapshot, and from that a
`Lean.Environment`, on the server-side. Widgets currently have to pass
this position around manually; this has led to
[errors](leanprover-community/ProofWidgets4@ca66ebb)
in user code. Furthermore, so far I have not encountered any situation
where it makes sense to modify the position; thus a context seems like a
preferable approach. If needed, the context can still be set by users.

I also had to update some package versions to have tests building again.
I hope that didn't break anything!
Vtec234 added a commit that referenced this issue Jun 5, 2024
Implementation of leanprover/lean4#2064.

Besides adding support for widget messages, this adds an `EnvPosContext`
that stores the position that a component is "about" (see the docstring
for more detail). This was originally proposed in #197 and eventually
dismissed (see #226 for a detailed discussion), but I think it warrants
a reconsideration. While Gabriel's point that there are many positions
around remains true, the `EnvPosContext` stores a very specific one.
This position is only used to retrieve a snapshot, and from that a
`Lean.Environment`, on the server-side. Widgets currently have to pass
this position around manually; this has led to
[errors](leanprover-community/ProofWidgets4@ca66ebb)
in user code. Furthermore, so far I have not encountered any situation
where it makes sense to modify the position; thus a context seems like a
preferable approach. If needed, the context can still be set by users.

I also had to update some package versions to have tests building again.
I hope that didn't break anything!
Vtec234 added a commit that referenced this issue Jun 16, 2024
Implementation of leanprover/lean4#2064.

Besides adding support for widget messages, this adds an `EnvPosContext`
that stores the position that a component is "about" (see the docstring
for more detail). This was originally proposed in #197 and eventually
dismissed (see #226 for a detailed discussion), but I think it warrants
a reconsideration. While Gabriel's point that there are many positions
around remains true, the `EnvPosContext` stores a very specific one.
This position is only used to retrieve a snapshot, and from that a
`Lean.Environment`, on the server-side. Widgets currently have to pass
this position around manually; this has led to
[errors](leanprover-community/ProofWidgets4@ca66ebb)
in user code. Furthermore, so far I have not encountered any situation
where it makes sense to modify the position; thus a context seems like a
preferable approach. If needed, the context can still be set by users.

I also had to update some package versions to have tests building again.
I hope that didn't break anything!
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants