Ed Ayers
7fabdf95d6
refactor: diffTag → diffStatus
...
Co-authored-by: Gabriel Ebner <gebner@gebner.org>
2022-10-06 13:06:31 -07:00
E.W.Ayers
506abff532
fix: replace highlight with diffTag
2022-10-06 13:06:31 -07:00
Ed Ayers
22bb798995
feat: datatypes for LSP code actions ( #1654 )
2022-09-28 09:07:39 +00:00
Mario Carneiro
85119ba9d1
chore: move Std.* data structures to Lean.*
2022-09-26 05:46:04 -07:00
Ed Ayers
2a6697e077
feat: goal-diffs ( #1610 )
2022-09-24 11:46:11 +02:00
Mario Carneiro
6392c5b456
chore: import reductions
2022-09-15 14:02:38 -07:00
Gabriel Ebner
f1b5fa53f0
chore: use new comment syntax
2022-09-14 08:26:17 -07:00
Mario Carneiro
158e182b8b
chore: move Bootstrap.Dynamic -> Init.Dynamic
2022-09-02 04:36:54 -07:00
Gabriel Ebner
3d6006885b
feat: use widget source from first snapshot
2022-09-01 16:57:03 +02:00
Gabriel Ebner
9bfbabb9df
fix: do not fail widget request after #exit
2022-09-01 16:57:03 +02:00
Gabriel Ebner
90f92c3a9e
fix: use delabAppExplicit for tooltips
2022-08-25 18:38:21 +02:00
Gabriel Ebner
e4a7b82c8d
feat: use interactive goals in messages
2022-08-15 08:55:25 -07:00
Gabriel Ebner
c7e45722a3
feat: trace nodes with messages
2022-08-15 08:55:25 -07:00
Mario Carneiro
014db5d6d0
doc: relocate doc strings from elab to syntax
2022-08-13 17:16:40 -07:00
Gabriel Ebner
e9545a426f
refactor: RpcEncodable
2022-08-10 06:31:46 -07:00
Leonardo de Moura
413db56b89
refactor: simplify runTermElabM and liftTermElabM
2022-08-07 07:35:02 -07:00
Wojciech Nawrocki
273bc683b9
feat: widget tutorial and general RequestM lifts
2022-08-06 11:54:44 -07:00
Mario Carneiro
ea0f177bf2
feat: add unused/deprecation diagnostic tags
2022-08-05 17:45:50 +02:00
Leonardo de Moura
642cf0bc6d
feat: add option pp.showLetValues
...
closes #1345
2022-07-26 17:53:34 -07:00
Wojciech Nawrocki
e30ae62dff
refactor: simplify position type
2022-07-25 08:01:27 -07:00
E.W.Ayers
b714e087d6
fix: widgetSourceRegistry now stores the UserWidgetDefinition declaration name instead of WidgetSource
...
This means that the environment extension is not storing a big text object and instead the text
is retrieved from the declaration itself.
2022-07-25 08:01:27 -07:00
E.W.Ayers
591b218607
doc: fix @kha issues
2022-07-25 08:01:27 -07:00
E.W.Ayers
28ebf90948
fix: add Inhabited Std.RBMap
2022-07-25 08:01:27 -07:00
E.W.Ayers
8deee553bb
fix: local instances
2022-07-25 08:01:27 -07:00
E.W.Ayers
67eae54c3d
style: userwidget
2022-07-25 08:01:27 -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
Wojciech Nawrocki
0824e6b22b
chore: rebase on 2022-07-10
2022-07-25 08:01:27 -07:00
Wojciech Nawrocki
625be05aa8
chore: use invalidParams error code
2022-07-25 08:01:27 -07:00
E.W.Ayers
4eb97a7954
refactor: getWidgetInfos → getWidgets
...
also rm hash field from UserWidgetInfo because it can be computed in handler instead.
2022-07-25 08:01:27 -07:00
E.W.Ayers
9b5be5a039
chore: remove Json.syntax docstring
2022-07-25 08:01:27 -07:00
E.W.Ayers
b7d70877f7
feat: user widgets
...
See #1225
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
eba400543d
refactor: use computed fields for Name
2022-07-11 14:19:41 -07:00
Sebastian Ullrich
2f67295c7d
feat: strengthen pp* signatures
2022-07-03 19:14:49 +02:00
E.W.Ayers
2fe933cdf5
refactor: make SubExpr.Pos a definition
...
Instead of an abbreviation. It is easier to understand
Pos operations in terms of 'push' and 'pop' rather than
through arithmetic.
2022-06-17 17:47:51 -07:00
E.W.Ayers
13e286f545
doc: fix docstring for InteractiveGoal
2022-06-13 16:32:01 -07: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
69facfbe8e
fix: remove Optional from InteractiveHypothesisBundle.fvarIds
2022-06-13 16:32:01 -07:00
E.W.Ayers
45e3c72be7
refactor: InteractiveHypothesis → InteractiveHypothesisBundle
2022-06-13 16:32:01 -07:00
Ed Ayers
5130da82a8
doc: src/Lean/Widget/InteractiveGoal.lean
...
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2022-06-13 16:32:01 -07:00
E.W.Ayers
cea53fc53e
fix: tests
...
Caused by a classic imperative programming bug oops
2022-06-13 16:32:01 -07:00
E.W.Ayers
f2a874ebaa
fix: handle inaccessible fvar names correctly
2022-06-13 16:32:01 -07:00
E.W.Ayers
675147dcfc
fix: make InteractiveHyp.fvarIds optional
...
This is for backwards compat.
2022-06-13 16:32:01 -07:00
E.W.Ayers
0f61d1dc59
refactor: key fields are now f/mvarid fields
2022-06-13 16:32:01 -07:00
E.W.Ayers
6e1c9653d9
feat: Add a key field to InteractiveGoal
...
This is used to uniquely identify InteractiveGoals and
InteractiveHypotheses. This makes it easier to do
contextual suggestions: eg the infoview can send a message
saying "the user clicked on subexpression 5 in hypothesis N in goal G"
where N and G are unique identifiers for a goal rather than pretty names
which may be non-unique or indices which may be difficult to compute
(eg in infoview there is a mode where hypotheses are reversed or filtered).
While adding these I also refactored the InteractiveGoal generating function.
I unwrapped a fold in to a for/in loop with mutating variables which is a
little easier to read.
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
