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

[client] Option to show goals on click #89

Closed
ejgallego opened this issue Dec 8, 2022 · 0 comments · Fixed by #116 or ocaml/opam-repository#22802
Closed

[client] Option to show goals on click #89

ejgallego opened this issue Dec 8, 2022 · 0 comments · Fixed by #116 or ocaml/opam-repository#22802
Milestone
0.1.1

Comments

@ejgallego
Copy link
Owner

No description provided.

@ejgallego ejgallego converted this from a draft issue Dec 8, 2022
@ejgallego ejgallego added this to the 0.1.1 milestone Dec 8, 2022
@ejgallego ejgallego moved this to Todo in coq-lsp roadmap Dec 22, 2022
ejgallego added a commit that referenced this issue Dec 26, 2022
@ejgallego
[goals] Show goals on click (+ configuration options).
23ac43e 
We allow to show goals on click, on cursor movement, or on
both. User-configurable.

Fixes #89
@ejgallego ejgallego mentioned this issue Dec 26, 2022
Merged
ejgallego added a commit that referenced this issue Dec 26, 2022
@ejgallego
[goals] Show goals on click (+ configuration options).
40e4f6b 
We allow to show goals on click, on cursor movement, or on
both. User-configurable.

Fixes #89
Repository owner moved this from Todo to Done in coq-lsp roadmap Dec 26, 2022
@ejgallego ejgallego mentioned this issue Dec 27, 2022
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Dec 27, 2022
@ejgallego
[new release] coq-lsp (0.1.1+v8.16)
96b7052 
CHANGES:

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

 - Don't crash if the log file can't be created (@ejgallego, ejgallego/coq-lsp#87)
 - Use LSP functions for client-side logging (@ejgallego, ejgallego/coq-lsp#87)
 - Log `_CoqProject` detection settings to client window (@ejgallego, ejgallego/coq-lsp#88)
 - Use plugin include paths from `_CoqProject` (@ejgallego, ejgallego/coq-lsp#88)
 - Support OCaml >= 4.12 (@ejgallego, ejgallego/coq-lsp#93)
 - Optimize the number of diagnostics sent in eager mode (@ejgallego, ejgallego/coq-lsp#104)
 - Improved syntax highlighting on VSCode client (@artagnon, ejgallego/coq-lsp#105)
 - Resume document checking from the point it was interrupted
   (@ejgallego, ejgallego/coq-lsp#95, ejgallego/coq-lsp#99)
 - Don't convert Coq "Info" messages such as "Foo is defined" to
   feedback by default; users willing to see them can set the
   corresponding option (@ejgallego, ejgallego/coq-lsp#113)
 - Send `$/coq/fileProgress` progress notifications from server,
   similarly to what Lean does; display them in Code's right gutter
   (@ejgallego, ejgallego/coq-lsp#106, fixes ejgallego/coq-lsp#54)
 - Show goals on click by default, allow users to configure the
   behavior to follow cursor in different ways (@ejgallego, ejgallego/coq-lsp#116,
   fixes ejgallego/coq-lsp#89)
 - Show file position in goal buffer, use collapsible elements for
   goal list (@ejgallego, ejgallego/coq-lsp#115, fixes ejgallego/coq-lsp#109)
 - Resume checking from common prefix on document update (@ejgallego,
   ejgallego/coq-lsp#111, fixes ejgallego/coq-lsp#110)
 - Only serve goals, hover, and symbols requests when the document
   has been sufficiently processed (@ejgallego, ejgallego/coq-lsp#120, fixes ejgallego/coq-lsp#100)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
coq-lsp roadmap
Archived in project
Milestone
0.1.1
1 participant
@ejgallego