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

82 commits

Author SHA1 Message Date
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
Sebastian Ullrich
51adfa2e0c fix: do not call lake print-paths for lakefile.lean 
Fixes #873
 2021-12-17 12:22:30 +01:00
Leonardo de Moura
34430cd7c3 fix: semantic highlighting for keywords of the form #<alpha>... 
closes #703
 2021-12-14 17:58:56 -08:00
Sebastian Ullrich
a4633d30e2 fix: option completion after trailing . 2021-12-10 14:19:19 -08:00
Leonardo de Moura
68bd55af32 chore: fix codebase 2021-12-10 13:12:09 -08:00
Joscha
d19cfede02 fix: implement suggestions 2021-12-10 15:25:43 +01:00
Joscha
e4406f1785 fix: find references to function parameters in function body 
With #861, the server can now connect the occurrences of parameters in the
function definition and in the function body to each other.
 2021-12-10 15:25:43 +01:00
Joscha
12ee541622 fix: reference fields in constructor correctly 2021-12-10 15:25:43 +01:00
Joscha
11ba6dc216 test: add simple "find references" test 2021-12-10 15:25:43 +01:00
Joscha
2823cbc87b feat: implement single-file "find references" in LSP server 2021-12-10 15:25:43 +01:00
Sebastian Ullrich
653ff184a8 fix: semantic highlighting, once more 2021-11-23 17:20:01 +01:00
Sebastian Ullrich
573c3c9760 fix: semantic highlighting, again 2021-11-23 17:02:09 +01:00
Sebastian Ullrich
226121433f fix: semantic highlighting of projection notation elaborated twice 2021-11-23 13:01:51 +01:00
Sebastian Ullrich
44f9edff87 feat: resolve symlinks in LEAN_SRC_PATH 2021-11-19 10:09:26 +01:00
Sebastian Ullrich
8df2b07209 refactor: remove double exception layer in RequestM 2021-11-09 16:58:13 +01:00
Sebastian Ullrich
e92f7f1b4b refactor: server: assume 1 info tree per snapshot 2021-11-04 18:31:36 +01:00
Wojciech Nawrocki
e843fb7ca5 fix: widget messages 2021-10-17 10:01:23 +02:00
Gabriel Ebner
d6ba8e597a feat: add range parameter to getInteractiveDiagnostics 2021-10-11 22:59:47 +02:00
Wojciech Nawrocki
07f99eba73 fix: use local context from Info node in widgets 2021-10-04 21:09:44 +02:00
Leonardo de Moura
42436254ee fix: code 2021-09-12 19:11:21 -07:00
Leonardo de Moura
391366ef24 refactor: add annotation for displaying conv state 2021-09-02 15:52:11 -07:00
Leonardo de Moura
1a362bc212 feat: add support for displaying conv goal in interactive mode 2021-09-01 16:45:12 -07:00
Wojciech Nawrocki
0897984a95 feat: send expression range in interactive term goal 2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
2f5fbf3b13 feat: support multiple RPC sessions 
Motivation: we may want to also use RPC in editor insets, or multiple
webviews in general.
 2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
03dbfaea03 chore: remove ExprWithCtx 2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
fd016c6065 chore: address some comments 2021-08-24 08:57:41 -07:00