Wojciech Nawrocki
ffc6efd5d0
fix: use properly random RPC session id
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
9a5cdaf506
chore: address review 1
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
f077dd05d3
feat: RPC ref decrement
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
80d90038ad
feat: add Format tags
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
d97e1b91ea
chore: drop RPC wrappers for now
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
b3316fd9c2
feat: RPC handlers
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
4d83e79121
feat: more RPC handlers
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
3ec568c110
feat: initial RPC
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
079c290ce0
feat: JSON serde for Name and USize
2021-07-24 10:45:28 +02:00
Daniel Fabian
0d41fd03f7
feat: add xml parser.
...
in order to generate the LLVM extern declarations we want to use a generator that spits out XML. Hence adding a small XML parser.
2021-07-13 09:58:27 -07:00
Wojciech Nawrocki
521ed11330
chore: move parseTagged
...
It should live in Lean.Data.Json.FromToJson because many modules import that but not Lean.Elab.Deriving.FromToJson.
2021-07-12 09:10:29 +02:00
Leonardo de Moura
f4a7ffd8c8
chore: fix codebase and tests
2021-06-29 17:14:52 -07:00
Sebastian Ullrich
cef3ade164
fix: info on non-atomic simp args
2021-06-23 00:08:07 -07:00
Sebastian Ullrich
eb1e285e26
chore: style
2021-06-21 10:17:26 -07:00
Gabriel Ebner
5786f58738
feat: plain term goal request
2021-06-07 16:23:22 -07:00
Sebastian Ullrich
0c3c0ed735
fix: ignore notifications in readResponseAs
2021-06-07 13:21:13 +02:00
Daniel Fabian
63d58c2f64
refactor: use Except instead of Option in the JSON code.
2021-06-07 12:10:10 +02:00
Gabriel Ebner
f50647e1c2
doc: describe non-standard requests and notifications
2021-06-05 13:49:28 +02:00
Gabriel Ebner
501c31da4d
feat: send $/lean/fileProgress notification
2021-06-05 13:49:28 +02:00
Leonardo de Moura
7424f9c8b0
chore: remove HashableUSize
2021-06-02 09:58:46 -07:00
Leonardo de Moura
d435b435c5
chore: remove workaround
2021-06-02 08:06:52 -07:00
Leonardo de Moura
5219593823
chore: use UInt64 to define Name
2021-06-02 08:00:23 -07:00
Leonardo de Moura
43812444a7
chore: Hashable => HashableUSize
2021-06-02 07:24:26 -07:00
Sebastian Ullrich
619873c842
feat: make System.FilePath opaque
2021-05-28 14:19:59 +02:00
Sebastian Ullrich
a02c6fd3eb
chore: adapt stdlib & tests
2021-05-20 15:17:36 -07:00
Sebastian Ullrich
23f0c1051c
feat: improve ToString/Quote Name
2021-05-19 09:34:01 +02:00
Sebastian Ullrich
3f9c015dd4
feat: pp.proofs & pp.proofs.withType
...
Resolves #210
2021-05-14 15:14:58 +02:00
Leonardo de Moura
8e81f03e3a
chore: adjust stdlib to recent changes
2021-05-06 15:43:56 -07:00
Daniel Fabian
0238bf8c33
refactor: use Ordering inside of rbmap instead of lt.
2021-04-27 07:58:58 -07:00
Leonardo de Moura
3a80e87793
chore: #405 step 1
2021-04-22 20:03:48 -07:00
Leonardo de Moura
5fc1a86274
chore: indentation
2021-04-11 22:00:21 -07:00
Leonardo de Moura
83b83f51e9
fix: resolveProvider?
...
Recent bug fixes exposed a problem here.
The field `resolveProvider?` has a `?`, but is not an `Option`
type. The `ToJson` makes this assumption and uses the auxiliary
function `opt`. The bugs fixed today were masjing this problem.
2021-04-11 21:45:59 -07:00
Leonardo de Moura
bc8daee635
fix: index out of bounds
2021-04-09 10:09:12 -07:00
Leonardo de Moura
9d12856432
feat: missing forM
2021-04-03 18:24:31 -07:00
Leonardo de Moura
20f569c033
feat: set_option completion
2021-04-03 15:06:50 -07:00
Leonardo de Moura
0a94aaabc9
feat: use expected type to prioritize completion candidates
2021-04-03 14:12:42 -07:00
Sebastian Ullrich
8f67921221
feat: Json.setObjVal!
2021-04-03 00:23:46 +02:00
Sebastian Ullrich
8440097e87
chore: server: repr-print invalid header
2021-04-03 00:23:45 +02:00
Sebastian Ullrich
63b96f62e7
feat: server: auto completion skeleton
2021-04-01 18:26:17 +02:00
Leonardo de Moura
4705532231
chore: add missing instance
2021-03-27 14:06:33 -07:00
Leonardo de Moura
b85c60aa75
chore: remove leftovers
2021-03-23 17:33:23 -07:00
Sebastian Ullrich
62ae39e62b
fix: pp.all should not turn off pp.binder_types
2021-03-23 19:45:41 +01:00
Leonardo de Moura
880f1372bd
feat: set pp.inaccessibleNames true when visualizing tactic state
...
@Kha The default value (false) for `pp.inaccessibleNames == false` help when
visualizing error messages (see test
`hidingInaccessibleNames.lean`). We added this feature after to hide
intermediate variables created by `match_syntax`.
However, this default value confused me in tactic mode. For example,
it will hide a hypotheses `x : Fin 0` if nobody depends on it, but as
a user we want to know we have it since we can close the goal using
it. Thus, I added `withPPInaccessibleNames act`, it executes `act`
using `pp.inaccessibleNames true` if the user did not explicitly set
it. I use this combinator at `FileWorker` and when producing the
`unsolved goals` error message. In all other scenarios, I believe
hiding these inaccessible variables is a good thing.
2021-03-21 18:21:46 -07:00
Leonardo de Moura
9a5f239513
refactor: remove Monad Option and Alternative Option
...
We should use `OptionM` instead.
`Option` still implements `Functor` and `OrElse`.
cc @Kha
2021-03-20 18:25:25 -07:00
Sebastian Ullrich
99d8e34a51
feat: server: highlight variables & field notation
2021-03-16 16:41:32 -07:00
Sebastian Ullrich
ddff87f7f5
feat: server: also implement full semantic token requests
...
because lsp-mode freaks out without them
2021-03-16 16:41:32 -07:00
Sebastian Ullrich
5df753f338
feat: server: support ranged semantic tokens (keywords only for now)
2021-03-16 16:41:32 -07:00
Sebastian Ullrich
048d592fe8
fix: FileMap out of bounds
2021-03-14 08:23:32 -07:00
Sebastian Ullrich
b6622d2bef
feat: server: preserve full range of messages
2021-03-10 17:09:41 +01:00
Sebastian Ullrich
c2f7ecaf37
feat: server: also transmit array of goals
2021-03-10 17:09:41 +01:00
