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

API to report progress to the GUI #12009

Open
JaroslavTulach opened this issue Jan 7, 2025 · 0 comments
Open

API to report progress to the GUI #12009

JaroslavTulach opened this issue Jan 7, 2025 · 0 comments
Assignees
@JaroslavTulach
Labels
-compiler -language-server -libs Libraries: New libraries to be implemented

Comments

@JaroslavTulach
Copy link
Member

I see progress field in Pending update. We could display node as being evaluated if progress != 0. If you know better API for this, please let me know.

Yes, that was my idea, when I introduced the progress field. Thus it'd be:

  • if there is no progress field, the node is pending and not yet being evaluated
  • if there is some value in progress field the node is pending and being evaluated

All that's needed is the IDE to use such info and language server to fill it.
@github-project-automation github-project-automation bot moved this to ❓New in Issues Board Jan 7, 2025
@JaroslavTulach JaroslavTulach self-assigned this Jan 7, 2025
@JaroslavTulach JaroslavTulach added -compiler -language-server -libs Libraries: New libraries to be implemented labels Jan 7, 2025
@JaroslavTulach JaroslavTulach mentioned this issue Jan 7, 2025
Open
@JaroslavTulach JaroslavTulach moved this from ❓New to 📤 Backlog in Issues Board Jan 7, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@JaroslavTulach JaroslavTulach

Labels
-compiler -language-server -libs Libraries: New libraries to be implemented
Projects
Issues Board
Status: 📤 Backlog
Milestone
No milestone
Development

No branches or pull requests
1 participant
@JaroslavTulach