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

[goals] Improve multi-goal, show position _à la Lean_ #109

Closed
ejgallego opened this issue Dec 22, 2022 · 2 comments · Fixed by #115 or ocaml/opam-repository#22802
Closed

[goals] Improve multi-goal, show position _à la Lean_ #109

ejgallego opened this issue Dec 22, 2022 · 2 comments · Fixed by #115 or ocaml/opam-repository#22802
Labels
kind: enhancement New feature or request part: goals and info panel
Milestone
0.1.1

Comments

@ejgallego
Copy link
Owner

No description provided.

@ejgallego ejgallego added this to the 0.1.1 milestone Dec 22, 2022
@Alizter
Copy link
Collaborator

Alizter commented Dec 23, 2022

What does Lean do?

@ejgallego
Copy link
Owner Author

  • it shows the point of the buffer for the goal at the top
  • puts every goal under a collapsible tree-like element (I think, need to double check that)

ejgallego added a commit that referenced this issue Dec 26, 2022
@ejgallego
[goals] Display position for goals, handle multiple goals better.
50d381d 
Fixes #109
@ejgallego ejgallego mentioned this issue Dec 26, 2022
Merged
ejgallego added a commit that referenced this issue Dec 26, 2022
@ejgallego
[goals] Display position for goals, handle multiple goals better.
a79b9dd 
Fixes #109
ejgallego added a commit that referenced this issue Dec 26, 2022
@ejgallego
[goals] Display position for goals, handle multiple goals better.
2d62070 
Fixes #109
ejgallego added a commit that referenced this issue Dec 26, 2022
@ejgallego
[goals] Display position for goals, handle multiple goals better.
fa1819d 
Still a long way to go, but this already looks much better.

Fixes #109
ejgallego added a commit that referenced this issue Dec 26, 2022
@ejgallego
[goals] Display position for goals, handle multiple goals better.
e2e4642 
Still a long way to go, but this already looks much better.

Fixes #109
@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
kind: enhancement New feature or request part: goals and info panel
Projects
None yet
Milestone
0.1.1
2 participants
@ejgallego @Alizter