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

Enable find widget in goal panel #309

Merged
merged 1 commit into from
Feb 9, 2023
Merged

Enable find widget in goal panel #309

merged 1 commit into from
Feb 9, 2023

Conversation

Alizter
Copy link
Collaborator

@Alizter Alizter commented Feb 9, 2023 •
edited
Loading

Fix #305

Tested and works.

@Alizter Alizter mentioned this pull request Feb 9, 2023
Closed
Alizter
Alizter commented Feb 9, 2023
View reviewed changes
editor/code/src/goals.ts
@@ -31,12 +31,14 @@ export class InfoPanel {
}

panelFactory() {
let webviewOpts: WebviewOptions = { enableScripts: true };
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was an intersection type so you couldn't add enableFindWidget here directly. I've inlined it but the type is really WebviewOptions & WebviewPanelOptions.

Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can also just remove the annotation (or add the intersection to the type annotation)

ejgallego
ejgallego approved these changes Feb 9, 2023
View reviewed changes
Copy link
Owner

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh, well spotted! Thanks a lot.

@ejgallego ejgallego added this to the 0.1.5 milestone Feb 9, 2023
@ejgallego
Copy link
Owner

There is a prettier failure, I will rebase, uninline, and add a changes entry.

@ejgallego
[goals] Enable find widget in goal panel
4103738 
Fixes ejgallego#305

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: e3066447-b19a-48c6-8222-3e15636591c8 -->
@ejgallego ejgallego force-pushed the ps/rr/enable_find_widget_in_goal_panel branch from bf56d00 to 4103738 Compare February 9, 2023 15:36
@ejgallego ejgallego merged commit cd545ee into ejgallego:main Feb 9, 2023
@Alizter Alizter deleted the ps/rr/enable_find_widget_in_goal_panel branch February 9, 2023 15:45
@ejgallego ejgallego mentioned this pull request Feb 15, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this pull request Feb 15, 2023
@ejgallego
[new release] coq-lsp (0.1.5+8.16)
b7a2330 
CHANGES:

---------------------

 - Fix a bug when trying to complete in an empty file (@ejgallego,
   ejgallego/coq-lsp#270)
 - Fix a bug with the position reported by the `$/coq/fileProgress`
   notification
 - Fix messages panel rendering after the port to React (@ejgallego,
   ejgallego/coq-lsp#272)
 - Fix non-compliance with LSP range type due to extra `offset` field
   (@ejgallego, ejgallego/coq-lsp#271)
 - The goal display now numbers goals starting with 1 instead of 0
   (@artagnon, ejgallego/coq-lsp#277, report by Hugo Herbelin)
 - Markdown Coq code blocks now must specify "coq" as a language
   (@ejgallego, ejgallego/coq-lsp#280)
 - Server is now more strict w.r.t. what URIs it will accept for
   documents, see protocol documentation (@ejgallego, ejgallego/coq-lsp#286, reported
   by Alex Sanchez-Stern)
 - Hypotheses with bodies are now correctly displayed (@ejgallego,
   ejgallego/coq-lsp#296, fixes ejgallego/coq-lsp#293, report by Ali Caglayan)
 - `coq-lsp` incorrectly required the optional `rootPath`
   initialization parameter, moreover it ignored `rootUri` if present
   which goes against the LSP spec (@ejgallego, ejgallego/coq-lsp#295, report by Alex
   Sanchez-Stern)
 - `coq-lsp` will now reject opening multiple files when the
   underlying Coq version is buggy (@ejgallego, fixes ejgallego/coq-lsp#275, fixes
   ejgallego/coq-lsp#281)
 - Fix bug when parsing client option for unicode completion
   (@ejgallego ejgallego/coq-lsp#301)
 - Support unicode characters in filenames (@artagnon, ejgallego/coq-lsp#302)
 - Stop checking documents after a maximum number of errors,
   user-configurable (by default 150) (@ejgallego, ejgallego/coq-lsp#303)
 - Coq Markdown files (.mv extension) are now highlighted properly
   using both Coq and Markdown syntax rules (@4ever2, ejgallego/coq-lsp#307)
 - Goal view now supports find (@Alizter, ejgallego/coq-lsp#309, closes ejgallego/coq-lsp#305)
 - coq-lsp now understands a basic version of Coq Waterproof files
   (.wpn) Note that we don't associate to them by default, as to allow
   the waterproof extension to take over the files (@ejgallego, ejgallego/coq-lsp#306)
 - URI validation is now more strict, and some further bugs should be
   solved; note still this can be an issue on some client settings
   (@ejgallego, ejgallego/coq-lsp#313, fixes ejgallego/coq-lsp#187)
 - Display Coq info and debug messages in info panel (@ejgallego,
   ejgallego/coq-lsp#314, fixes ejgallego/coq-lsp#308)
 - Goal display handles background goals better, showing preview,
   goals stack, and focusing information (@ejgallego, ejgallego/coq-lsp#290, fixes
   ejgallego/coq-lsp#288, fixes ejgallego/coq-lsp#304, based on jsCoq code by Shachar Itzhaky)
 - Warnings are now printed in the info view messages panel
   (@ejgallego, ejgallego/coq-lsp#315, fixes ejgallego/coq-lsp#195)
 - Info protocol messages now have location and level
   (@ejgallego, ejgallego/coq-lsp#315)
 - Warnings are not printed in the info view messages panel
   (@ejgallego, #, fixes ejgallego/coq-lsp#195)
 - Improved `documentSymbol` return type for newer `DocumentSymbol[]`
   hierarchical symbol support. This means that sections and modules
   will now be properly represented, as well as constructors for
   inductive types, projections for records, etc...  (@ejgallego,
   ejgallego/coq-lsp#174, fixes ejgallego/coq-lsp#121, ejgallego/coq-lsp#122)
 - [internal] Error recovery can now execute full Coq commands as to
   amend states, required for ejgallego/coq-lsp#319 (@ejallego, ejgallego/coq-lsp#320)
 - Auto-admit the previous bullet goal when a new bullet cannot be
   opened due to an unsolved previous bullet. This also works for {}
   focusing operators. This is very useful when navigating bulleted
   proofs (@ejgallego, @Alizter, ejgallego/coq-lsp#319, fixes ejgallego/coq-lsp#300)
 - Store Ast.Info.t incrementally (@ejgallego, ejgallego/coq-lsp#337, fixes ejgallego/coq-lsp#316)
 - Basic jump to definition support; due to lack of workspace
   metadata, this only works inside the same file (@ejgallego, ejgallego/coq-lsp#318)
 - Show type of identifiers at point on hover (@ejgallego, ejgallego/coq-lsp#321, cc:
   ejgallego/coq-lsp#164)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ejgallego ejgallego ejgallego approved these changes

Assignees
No one assigned
Labels
kind: enhancement New feature or request kind: HCI design part: client (VSCode) part: goals and info panel
Projects
None yet
Milestone
0.1.5
Development

Successfully merging this pull request may close these issues.

Support find in the goal window
2 participants
@Alizter @ejgallego