E.W.Ayers
f52a1bd37c
doc: JSON-RPC
2022-08-26 20:49:57 -07:00
E.W.Ayers
2e99e8c22d
feat: Float ↔ Json
2022-08-16 08:01:23 -07:00
Wojciech Nawrocki
42fec60b01
fix: printing of integral JsonNumbers
2022-08-11 13:27:37 -07:00
Gabriel Ebner
e9545a426f
refactor: RpcEncodable
2022-08-10 06:31:46 -07:00
Wojciech Nawrocki
273bc683b9
feat: widget tutorial and general RequestM lifts
2022-08-06 11:54:44 -07:00
Chris Lovett
c4121e779d
fix: hexDigit ('a' ≤ c ∧ c ≤ 'f')
2022-08-05 14:08:03 -07:00
Mario Carneiro
ea0f177bf2
feat: add unused/deprecation diagnostic tags
2022-08-05 17:45:50 +02:00
Mario Carneiro
c952c69690
feat: add missingDocs linter
2022-07-31 18:18:21 -07:00
Mario Carneiro
42a4f2f451
feat: ForIn instance for NameMap and PersistentHashMap
2022-07-31 15:42:26 -07:00
Leonardo de Moura
a489bdb107
doc: some doc strings
2022-07-30 21:18:50 -07:00
Leonardo de Moura
fbc6bcff92
chore: remove unnecessary french quotes
2022-07-29 20:53:01 -07:00
Ed Ayers
c3f58a7eab
feat: add a message if Lean 4 is called with the Lean 3 extension
2022-07-29 11:08:51 +00:00
Leonardo de Moura
ed7f502e54
feat: doc string support for register_simp_attr, register_option, register_builtin_option, declare_config_elab
...
see #1374
2022-07-26 18:46:23 -07:00
E.W.Ayers
18a3d1a34e
fix: widgets are now defined using a UserWidgetDefinition
...
To satisfy https://github.com/leanprover/lean4/pull/1238#discussion_r908839474
2022-07-25 08:01:27 -07:00
Mario Carneiro
f6211b1a74
chore: convert doc/mod comments from /- to /--//-! ( #1354 )
2022-07-22 12:05:31 -07:00
Gabriel Ebner
4d5515ab0c
fix: do not use native_decide
2022-07-22 13:06:04 +02:00
tydeu
bd7739d02e
chore: add sanity check for SemanticTokenType/Modifier.names
2022-07-21 18:36:52 +02:00
tydeu
9d4a72bf6a
feat: up to spec SemanticTokens/Type/Modifier
2022-07-19 11:57:57 +02:00
Gabriel Ebner
eba400543d
refactor: use computed fields for Name
2022-07-11 14:19:41 -07:00
Leonardo de Moura
58619291e9
feat: better qualified name support in recursive definitions
2022-07-07 20:15:25 -07:00
Leonardo de Moura
2ebcf29cde
chore: use a[i]! for array accesses that may panic
2022-07-02 15:12:05 -07:00
Mariana Alanis
198179d0cc
fix: add a better handling in case only worker crashes (apply CR comments)
2022-06-15 18:40:44 -07:00
Mariana Alanis
4d7d82af86
fix: add a better handling in case only worker crashes (CR comments)
2022-06-15 18:40:44 -07:00
Mariana Alanis
6b75ca9734
fix: add a better handlng in case only worker crashes (and server stays available)
2022-06-15 18:40:44 -07:00
Leonardo de Moura
77ae79be46
chore: use let/if in do blocks
2022-06-13 17:10:14 -07:00
Leonardo de Moura
041827bed5
chore: unused variables
2022-06-07 17:54:10 -07:00
Sebastian Ullrich
f9e2a65f75
chore: further cleanup
...
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2022-06-07 16:37:45 -07:00
Sebastian Ullrich
8eefbf5227
chore: further clean up refactored code
2022-06-07 16:37:45 -07:00
Sebastian Ullrich
fb2a2b3de2
fix: fixup previous commit
2022-06-07 16:37:45 -07:00
Sebastian Ullrich
ae7b895f7a
refactor: unname some unused variables
2022-06-07 16:37:45 -07:00
Wojciech Nawrocki
8c5cebfb11
chore: default optional LSP fields
2022-05-31 00:07:56 +02:00
Wojciech Nawrocki
25a8646a5f
feat: add showDocument client capability
2022-05-31 00:07:56 +02:00
Leonardo de Moura
c65537aea5
feat: Option is a Monad again
...
TODO: remove `OptionM` after update stage0
see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084
2022-05-04 15:27:42 -07:00
Sebastian Ullrich
9b4feb3d13
perf: work around missed TCO
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
larsk21
235b6d8f69
fix: remove unnecessary fuzzy scoring rule
2022-04-11 16:08:55 +02: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
Leonardo de Moura
90c442da76
feat: add internal option for communicating to the delaborator that input term is a pattern
2022-03-16 07:50:29 -07:00
Lars
95cf18457d
chore: address review comments
2022-03-12 13:25:35 +00:00
larsk21
e430496903
doc: fix fuzzy matching docs
2022-03-11 16:25:26 -08:00
larsk21
ea5b6d568f
fix: review suggestions + code structure
2022-03-11 16:25:26 -08:00
Sebastian Ullrich
ff11325fce
perf: use mkArray in fuzzyMatchCore
2022-03-11 16:25:26 -08:00
Sebastian Ullrich
d48c5b99e9
perf: eliminate MProd allocations in iterateLookaround
2022-03-11 16:25:26 -08:00
Sebastian Ullrich
896b9b48a3
perf: eliminate some allocations in iterateLookaround
2022-03-11 16:25:26 -08:00
Sebastian Ullrich
7106d3fb34
perf: specialize iterateLookaround
2022-03-11 16:25:26 -08:00
larsk21
135eac71a1
feat: add string fuzzy matching
2022-03-11 16:25:26 -08:00
Leonardo de Moura
d6b782f811
chore: remove workaround
...
for regression introduced by the following change
* Auto implicit behavior changed for inductive families. An auto implicit argument occurring in inductive family index is also treated as an index (IF it is not fixed, see next item)
2022-03-08 17:58:20 -08: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
