Skip to content

Conversation

@ejgallego
Copy link
Owner

We need to do a setTimeout here to avoid flicker.

@ejgallego ejgallego marked this pull request as draft January 22, 2023 20:10
ejgallego added a commit that referenced this pull request Jan 23, 2023
This is prerequisite to implement / fix effectively #143 and #216 for
example; the current Info View rendering using strings doesn't scale
anymore to the kind of DOM manipulation we need.

Why React? That was a careful choice for many reasons, in particular
seems like the best fit for our use case (so far); moreover, 3rd party
package support is the best.
@ejgallego ejgallego added this to the 0.1.4 milestone Jan 23, 2023
ejgallego added a commit that referenced this pull request Jan 23, 2023
This is prerequisite to implement / fix effectively #143 and #216 for
example; the current Info View rendering using strings doesn't scale
anymore to the kind of DOM manipulation we need.

Why React? That was a careful choice for many reasons, in particular
seems like the best fit for our use case (so far); moreover, 3rd party
package support is the best.
ejgallego added a commit that referenced this pull request Jan 23, 2023
This is prerequisite to implement / fix effectively #143 and #216 for
example; the current Info View rendering using strings doesn't scale
anymore to the kind of DOM manipulation we need.

Why React? That was a careful choice for many reasons, in particular
seems like the best fit for our use case (so far); moreover, 3rd party
package support is the best.
ejgallego added a commit that referenced this pull request Jan 24, 2023
This is prerequisite to implement / fix effectively #143 and #216 for
example; the current Info View rendering using strings doesn't scale
anymore to the kind of DOM manipulation we need.

Why React? That was a careful choice for many reasons, in particular
seems like the best fit for our use case (so far); moreover, 3rd party
package support is the best.
ejgallego added a commit that referenced this pull request Jan 25, 2023
This is prerequisite to implement / fix effectively #143 and #216 for
example; the current Info View rendering using strings doesn't scale
anymore to the kind of DOM manipulation we need.

Why React? That was a careful choice for many reasons, in particular
seems like the best fit for our use case (so far); moreover, 3rd party
package support is the best.
@ejgallego ejgallego modified the milestones: 0.1.4, 0.1.5 Jan 25, 2023
ejgallego added a commit that referenced this pull request Jan 27, 2023
This is prerequisite to implement / fix effectively #143 and #216 for
example; the current Info View rendering using strings doesn't scale
anymore to the kind of DOM manipulation we need.

Why React? That was a careful choice for many reasons, in particular
seems like the best fit for our use case (so far); moreover, 3rd party
package support is the best.
ejgallego added a commit that referenced this pull request Jan 27, 2023
This is prerequisite to implement / fix effectively #143 and #216 for
example; the current Info View rendering using strings doesn't scale
anymore to the kind of DOM manipulation we need.

Why React? That was a careful choice for many reasons, in particular
seems like the best fit for our use case (so far); moreover, 3rd party
package support is the best.
ejgallego added a commit that referenced this pull request Jan 27, 2023
This is prerequisite to implement / fix effectively #143 and #216 for
example; the current Info View rendering using strings doesn't scale
anymore to the kind of DOM manipulation we need.

Why React? That was a careful choice for many reasons, in particular
seems like the best fit for our use case (so far); moreover, 3rd party
package support is the best.
ejgallego added a commit that referenced this pull request Jan 27, 2023
This is prerequisite to implement / fix effectively #143 and #216 for
example; the current Info View rendering using strings doesn't scale
anymore to the kind of DOM manipulation we need.

Why React? That was a careful choice for many reasons, in particular
seems like the best fit for our use case (so far); moreover, 3rd party
package support is the best.
@ejgallego ejgallego modified the milestones: 0.1.5, 0.1.6 Feb 6, 2023
@ejgallego ejgallego modified the milestones: 0.1.6, 0.1.7 Feb 21, 2023
@ejgallego ejgallego force-pushed the goals_show_info_waiting branch from a7c1a3c to 913ccb2 Compare February 22, 2023 03:37
We need to do a setTimeout here to avoid flicker.
@ejgallego ejgallego force-pushed the goals_show_info_waiting branch from 913ccb2 to 69c925e Compare March 16, 2023 23:36
@ejgallego ejgallego modified the milestones: 0.1.7, 0.1.8 Jun 13, 2023
@ejgallego ejgallego modified the milestones: 0.1.8, 0.1.9 Jul 7, 2023
@ejgallego ejgallego modified the milestones: 0.1.9, 0.3.0 Oct 2, 2023
@ejgallego ejgallego closed this Nov 27, 2025
@github-project-automation github-project-automation bot moved this from In Progress to Done in coq-lsp roadmap Nov 27, 2025
@ejgallego ejgallego marked this pull request as ready for review November 27, 2025 14:30
@ejgallego ejgallego deleted the goals_show_info_waiting branch November 27, 2025 14:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

Status: Done

Development

Successfully merging this pull request may close these issues.

2 participants