max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
28441 commits 1 branch 0 tags 5.3 GiB
Commit graph

107 commits

Author SHA1 Message Date
Sebastian Ullrich
86cd656fc6 refactor: adapt raw syntax manipulations to TSyntax 
Sometimes there's just no structure to work on
 2022-06-27 22:37:02 +02:00
Sebastian Ullrich
8979ed42a4 refactor: file worker: wait on header task before dispatching requests 2022-06-24 19:02:00 +02:00
Sebastian Ullrich
e14b4ab0e4 feat: file worker: make header snapshot asynchronous 2022-06-24 19:02:00 +02:00
E.W.Ayers
2edf02544e chore: rm ExprWithCtx 
We will make this a separate PR
 2022-06-13 16:32:01 -07:00
E.W.Ayers
367bde3601 chore: revert "refactor: replace InfoWithCtx with ExprWithCtx" 
This reverts commit db342793d53c986b8794084196552c33711f9091.
 2022-06-13 16:32:01 -07:00
E.W.Ayers
f64cb95eca refactor: replace InfoWithCtx with ExprWithCtx 
This is potentially controversial. There are still some [todo]s that need sorting.
 2022-06-13 16:32:01 -07:00
E.W.Ayers
3d561a3ab0 doc: add docstrings for interactive 2022-06-13 16:32:01 -07:00
E.W.Ayers
e3d2080232 refactor: PPExprTaggedRequest -> PPExprTaggedParams 2022-06-13 16:32:01 -07:00
E.W.Ayers
fd66e70d1e fix: explicit structure for PPExprTaggedRequest 2022-06-13 16:32:01 -07:00
Wojciech Nawrocki
351be06a21 feat: ppExprTagged RPC call 2022-06-13 16:32:01 -07:00
Leonardo de Moura
041827bed5 chore: unused variables 2022-06-07 17:54:10 -07:00
Sebastian Ullrich
ae7b895f7a refactor: unname some unused variables 2022-06-07 16:37:45 -07:00
larsk21
b556e73657 refactor: extend Lsp.ModuleRefs in Server.References 2022-06-03 13:03:52 +02:00
Leonardo de Moura
484e510221 feat: do not use pp.inaccessibleNames = true at getInteractiveTermGoal 
See discussion at https://github.com/leanprover/vscode-lean4/issues/76

We also use `pp.inaccessibleNames = false` in error messages. In this
setting, an inaccessible name is displayed in the context only if the
target type depends on it.
 2022-06-02 16:22:43 -07:00
Wojciech Nawrocki
115c564b18 feat: go to head constant in applications 
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
cd47c30e47 chore: review fixes 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
8c67afae2f feat: generalize getGoToLocation RPC 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
aef8d32d0b feat: add RPC call to retrieve defn/decl/type defn 2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
9c058a5798 chore: remove some unnecessary partial 2022-05-31 00:07:56 +02:00
Sebastian Ullrich
b31690b1d7 fix: go to definition/goal state at end of syntax 2022-05-30 11:16:25 +02:00
Wojciech Nawrocki
603a062f1f chore: revert API change 2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
63b33424e1 feat: add Widget.Basic 2022-05-12 08:38:09 -07:00
Wojciech Nawrocki
81b1f1df6e refactor: unify format functions 2022-05-12 08:38:09 -07:00
Sebastian Ullrich
a167828b79 fix: refine previous commit's heuristic 
Show indented state if there is no outer state that is leading & not indented
relative to the cursor position
 2022-04-29 16:16:09 +02:00
Leonardo de Moura
2a2aeec085 feat: LSP semantic token for where and let rec declarations 2022-04-22 09:52:20 -07:00
Leonardo de Moura
4727fd6883 feat: do not hightlight auxiliary declarations used to compile recursive definitions as variables 
They are "morally" constants.
 2022-04-21 08:11:22 -07:00
Leonardo de Moura
de2e2447d2 chore: style 2022-04-07 17:35:05 -07:00
Wojciech Nawrocki
9223bf3640 feat: environment extension for RPC procedures 2022-03-26 06:26:41 -07:00
Leonardo de Moura
3862e7867b refactor: make String.Pos opaque 
TODO: this refactoring exposed bugs in `FuzzyMatching` and `Lake`

closes #410
 2022-03-20 10:47:13 -07:00
Sebastian Ullrich
147a5c2933 chore: prefer LEAN_SRC_PATH 2022-03-14 17:24:25 +01:00
Jonathan Coates
11cce61e4d chore: Clean up LSP folding a little 
- Wait for all terms to be elaborated before showing folding regions.
   May want to change this to support partial results.
 - Use .span to extract import statements, rather than mutually
   recursive functions.
 - Some tiny other bits of cleanup
 2022-03-07 17:23:35 +01:00
Jonathan Coates
04e60cebd1 feat: LSP code folding support 
The following constructs are foldable:
 - Sections and namespaces
 - Blocks of import/open statements
 - Multi-line commands (so mostly definitions)
 - Mutual definitions
 - Module-level doc comments
 - Top-level definition doc comments

Fixes #1012
 2022-03-07 17:23:35 +01:00
Sebastian Ullrich
6c6f66b812 feat: propagate actual file name in file worker 
Also stop recreating the FileMap for every command, that's quadratic!
 2022-02-27 10:33:27 +01:00
Sebastian Ullrich
2390691116 chore: remove obsolete workaround 2022-02-11 18:19:59 +01:00
Joscha
196cf67eed fix: handle overlapping definitions 2022-02-06 16:52:18 +01:00
Leonardo de Moura
12e2a79170 chore: fix codebase after removing auto pure 2022-02-03 18:08:14 -08:00
larsk21
bc65da2e83 feat: extend handleDocumentHighlight 2022-02-02 13:03:21 +01:00
Wojciech Nawrocki
2d1cea0864 feat: inform server if widgets are available 2022-01-29 10:04:25 +01:00
Leonardo de Moura
2192e6148b chore: remove coe, coeSort, and coeFun abbreviations 
The notation `↑ e` is now expanded eagerly.

See #403
 2022-01-20 15:19:06 -08:00
Leonardo de Moura
be4c86f780 chore: remove temporary workarounds 2022-01-17 17:03:15 -08:00
Leonardo de Moura
f8653a8cb7 chore: add temporary workaround 2022-01-17 16:58:39 -08:00
Leonardo de Moura
b970919978 chore: remove unnecessary Inhabited 2022-01-14 19:48:10 -08:00
larsk21
b712918db9 fix: unify handleDefinition for imports 2022-01-14 10:32:06 +01:00
larsk21
ecaa004dcc feat: make withWaitFindSnap consider all snaps of a document 2022-01-14 10:32:06 +01:00
larsk21
e584560b17 feat: enable "go to definition" for imports 2022-01-14 10:32:06 +01:00
Sebastian Ullrich
d503fe6d13 refactor: avoid double exception layer with AsyncList 2022-01-14 09:18:57 +01:00
Joscha
088433dc57 refactor: let AsyncList creation be stateful 2022-01-14 09:18:57 +01:00
Joscha
7abdf94fc5 feat: respond to reference request in watchdog 2022-01-14 09:18:57 +01:00
Gabriel Ebner
dc65bb080a fix: race condition in RPC request handler 2022-01-10 13:37:40 +01:00
Gabriel Ebner
f146d456ce fix: only enable InsertReplaceEdit if supported 2022-01-07 20:28:10 +01:00