Skip to content
Snippets Groups Projects
Unverified Commit d7a745e9 authored by isovector's avatar isovector Committed by GitHub
Browse files

Wingman: streaming tactic solutions (#2102)


* WIP abstract LSP, take the pain out of writing LSP stuff

* Finish making commands

* Separate code lenses and actions

* Pull out types

* Finalize the abstract API

* Bug fix in JSON; first connected abstract handler

* Add ContinuationResult for better control over how edits work

* Remove IO from TacticProviders; use LspEnv instead

* installInteractions

* Pull TacticCodeActions into their own file

* Misc cleanup

* Haddock

* Fix bug in codelens

* Port EmptyCase to Interaction

* Rename makeTacticCodeAction -> makeTacticInteraction

* Support for partial timeouts in upcoming refinery v5

* asum instead of choice for assumption

* Don't count it as using a term if you only destruct it

* Let interactions return multiple results --- aka also info messages

* Update refinery lower bounds

* Revert "Update refinery lower bounds"

This reverts commit 53199b3b781884d7bd85ac8fb3efa1d2da915ea6.

* Pull refinery from the future

* Fix tests

* Add -XNumDecimals

* Fix AutoTypeLevel test

* Continue to emit errors

Co-authored-by: default avatarmergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
parent ed37b61f
No related branches found
No related tags found
No related merge requests found
Showing
with 267 additions and 85 deletions
Loading
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment