Skip to content

Removed { as trigger#333

Merged
rayman2000 merged 1 commit into
masterfrom
nklose/better-completions
Feb 5, 2026
Merged

Removed { as trigger#333
rayman2000 merged 1 commit into
masterfrom
nklose/better-completions

Conversation

@rayman2000

Copy link
Copy Markdown
Contributor

No description provided.

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Pull request overview

This pull request removes the "{" character as a completion trigger and adds a new SignatureHelp utility file for LSP functionality.

Changes:

  • Removed "{" from the list of completion trigger characters in Receiver.scala
  • Added new SignatureHelp.scala file defining LSP signature help types

Reviewed changes

Copilot reviewed 1 out of 2 changed files in this pull request and generated no comments.

File Description
src/main/scala/viper/server/frontends/lsp/ast/utility/SignatureHelp.scala Introduces new trait and case classes for signature help functionality, providing structured types for displaying function/method signatures
src/main/scala/viper/server/frontends/lsp/Receiver.scala Removes "{" from completion trigger characters, now only triggering on ".", ":", "(", and "["

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

@rayman2000 rayman2000 added this pull request to the merge queue Feb 5, 2026
@github-merge-queue github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Feb 5, 2026
@rayman2000 rayman2000 added this pull request to the merge queue Feb 5, 2026
@github-merge-queue github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Feb 5, 2026
@rayman2000 rayman2000 added this pull request to the merge queue Feb 5, 2026
Merged via the queue into master with commit 41adee8 Feb 5, 2026
24 of 25 checks passed
@rayman2000 rayman2000 deleted the nklose/better-completions branch February 5, 2026 18:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants