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

[frontend] Use coq-lsp view which in turn is jsCoq view converted to React #336

Merged
merged 8 commits into from Aug 17, 2023
Merged

[frontend] Use coq-lsp view which in turn is jsCoq view converted to React #336

merged 8 commits into from Aug 17, 2023

Conversation

ejgallego
Copy link
Member

No description provided.

@ejgallego ejgallego changed the base branch from v8.17 to v8.16+lsp July 26, 2023 15:23
@ejgallego ejgallego added this to the 0.17.0+lsp milestone Jul 26, 2023
@ejgallego ejgallego mentioned this pull request Jul 27, 2023
Open
24 tasks
@ejgallego ejgallego force-pushed the v8.16+lsp branch 2 times, most recently from 299510a to 06b986d Compare July 28, 2023 23:42
@ejgallego ejgallego force-pushed the v8.17+lsp+goalview branch 3 times, most recently from e25a7f3 to 30e0f20 Compare July 29, 2023 20:29
Base automatically changed from v8.16+lsp to v8.17+lsp August 9, 2023 13:02
@ejgallego
Copy link
Member Author

@corwin-of-amber this branch now only contains the new Goal View UI, we can merge when we think it is ready.

@ejgallego ejgallego mentioned this pull request Aug 9, 2023
Open
@corwin-of-amber
[ui] Style adjustments for goal view.
6d9df75 
Restored the splash screen. The info view is hidden until needed.
@corwin-of-amber
[ui] Dark mode for goal view.
d4cf965
@corwin-of-amber
[cleanup] Got rid of my_fflate.ts.
c8fa363 
Probably `fflate-unzip` is inconsistent because it does not have a
`'type': 'module'` field.
Should check.
@corwin-of-amber
[port] Corrected package reload.
aae9aa2 
Still does not work, blocked by the workspace refresh capability of the worker.
@corwin-of-amber
[ui] [feature] Proper splitter w/ dragging.
8ef46a4 
For flex layout (fixed layout rip probably).
@corwin-of-amber
[cleanup] Removed the toggled CSS class.
4c649e0 
It was confusing.
@corwin-of-amber
[feature] Persist split ratio.
b80636e
@corwin-of-amber corwin-of-amber merged commit a796825 into v8.17+lsp Aug 17, 2023
@ejgallego ejgallego deleted the v8.17+lsp+goalview branch August 18, 2023 14:21
@ejgallego
Copy link
Member Author

ejgallego commented Aug 18, 2023 •
edited

Great, thanks Shachar! It is looking pretty nice IMHO.

Is there any change you would like to get upstreamed to the view?

(I'm trying to figure out a better setup for sharing the view)

@corwin-of-amber
Copy link
Member

I did not make changes to the view itself but you can look at iframe.css and see if you want to borrow some of the styling (in particular, limiting the height of the error subpanel).
I want to make the tree view more customizable. Esp. being able to hide the top row (which currently shows :0:0) and also the messages subtree when there are no messages. Also, we should experiment with the goal view when there are multiple goals, in order to save some vertical space.

@corwin-of-amber
Copy link
Member

The parenthesized numbers are inconsistent. In Goals (2) they denote the number of goals. In Goal (1) it is a serial number. That's potentially counterintuitive.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
kind: ui
Projects
None yet
Milestone
0.17.0+lsp
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@ejgallego @corwin-of-amber