David Christiansen
9169a7aaa3
feat(emacs): Add a right-click menu to the Emacs mode
...
The right-click menu is computed from a list of functions that produce
menu items based on Lean server information. Each menu item is a
string and a closure to be invoked if the menu item is selected.
There are currently two menu features: "Find definition" works where
M-. does, and on holes, the menu includes the hole commands from the
server.
2017-06-16 12:23:55 +02:00
Leonardo de Moura
9b250a2fb8
fix(frontends/lean/interactive): hole_commands
2017-06-15 17:03:40 -07:00
Leonardo de Moura
fe774a25cf
chore(tests/lean/interactive): fix tests
2017-06-15 10:56:09 -07:00
Leonardo de Moura
bf0d785888
feat(library/messages, frontends/lean): optional end position for messages
...
We need this information to be able to fix issues with the transient
message boxes feature (#1667 ).
2017-06-15 10:47:58 -07:00
Leonardo de Moura
5cb96c7fa3
feat(frontends/lean): add option for pretty printing metavars, sorry and delayed abstractions as holes
...
This option is false by default, but true when executing hole commands
2017-06-15 10:24:26 -07:00
Leonardo de Moura
f0e5cc33c3
fix(frontends/lean/interactive): issue at https://github.com/leanprover/lean/pull/1671#discussion_r122243609
2017-06-15 09:43:08 -07:00
Gabriel Ebner
5528a26592
fix(library/tactic/tactic_state): make tactic.sleep interruptible
...
Fixes leanprover/vscode-lean#52
2017-06-15 17:16:40 +02:00
Gabriel Ebner
028c31779d
fix(frontends/lean/interactive): revert hole end column
...
I have tested this change in both emacs and vscode, and replacements
work correctly.
This reverts commit 6c2a144950
2017-06-15 17:01:10 +02:00
Leonardo de Moura
e99786afcd
fix(frontends/lean): do not store duplicate holes
2017-06-15 07:53:38 -07:00
Leonardo de Moura
7b69d829c3
doc(changes): add hole command feature
2017-06-15 07:40:19 -07:00
Leonardo de Moura
6c2a144950
fix(frontends/lean/interactive): hole end column
2017-06-15 07:36:11 -07:00
Leonardo de Moura
ba25d4876e
feat(frontends/lean/info_manager): multi-line holes
2017-06-15 07:23:06 -07:00
David Christiansen
a7a2e9a997
feat(emacs): Make display of message boxes more compact
...
Message boxes are now displayed without caption (which is available in
a tooltip). Additionally, single-line messages are displayed to the
right of the line that caused them, instead of underneath.
2017-06-15 14:15:07 +02:00
David Christiansen
043fe41d38
feat(emacs): Immediately toggle display of messages in Emacs
...
Now, message display is toggled immediately rather than waiting for a
keypress.
2017-06-15 14:15:07 +02:00
David Christiansen
7b3a71b438
feat(emacs): Add the display of Lean messages in transient boxes
...
Informational output is usually seen in Flycheck in lean-mode. Now, it
can also be displayed in transient boxes that are not really part of
the buffer. This allows them to be quickly visually compared.
2017-06-15 14:15:07 +02:00
David Christiansen
27feb14f73
feat(emacs): Add a message hook to the Emacs mode
...
When the server protocol returns a message, call user-defined hooks
with that message. This enables custom display of messages in addition
to Flycheck.
2017-06-15 14:15:07 +02:00
Gabriel Ebner
a001e85d82
fix(frontends/lean/builtin_exprs): set hole position after final token
2017-06-15 11:35:43 +02:00
David Christiansen
f3b66b3cfb
feat(emacs): Add support for the new holes feature to Emacs
...
Add the lean-hole command to Emacs, which queries the server for a
list of relevant hole commands, presents them to the user, and
executes the one that is selected.
The default keybinding is C-c SPC.
2017-06-15 10:27:43 +02:00
Gabriel Ebner
437ab1fc27
feat(server): add command to get all holes in a file
2017-06-15 10:23:26 +02:00
Gabriel Ebner
b09fee680c
fix(frontends/lean/info_manager): only store holes once
2017-06-15 10:22:48 +02:00
Leonardo de Moura
bce1f10ae4
doc(doc/changes): add missing features/changes
2017-06-14 23:12:18 -07:00
Jeremy Avigad
a045b0f00c
feat(doc/changes.md): create change log
2017-06-14 22:42:08 -07:00
Leonardo de Moura
3700bb4568
chore(library/tactic/hole_command,frontends/lean/interactive): fix style
2017-06-14 22:23:25 -07:00
Leonardo de Moura
7557a9e000
feat(shell/server,frontends/lean): add "hole_commands" server command
...
The new command returns the list of registered/applicable hole
commands.
2017-06-14 22:16:34 -07:00
Leonardo de Moura
7528e14e68
feat(frontends/lean,shell/server): "hole" command
2017-06-14 21:56:17 -07:00
Leonardo de Moura
c0556df2ec
feat(shell/server): add "hole" server command skeleton
2017-06-14 11:44:32 -07:00
Leonardo de Moura
55c8627f2c
feat(frontends/lean): {! ... !} takes a list of pre-terms
2017-06-13 22:19:17 -07:00
Leonardo de Moura
dac6eec556
feat(library/tactic): add hole_command bookkeeping
2017-06-13 21:12:29 -07:00
Leonardo de Moura
bb2c39b471
feat(frontends/lean): add hole notation {! ... !}
...
Holes {! ... !} are elaborated using `sorry`.
We report an error if their value is fixed by typing and/or
elaboration rules.
We store the tactic_state and the optional attribute in the
info_manager. The idea is to allow users to execute commands with
respect to the stored tactic state and optional attribute.
The optional attribute is a pre term.
We are planning to add commands such as:
- Check type of the given argument.
- Reduce the given argument.
- Synthesize the hole automatically, where the given argument encodes
hint to the synthesizer.
- Use the given argument to fill the hole.
2017-06-13 18:53:05 -07:00
Johannes Hölzl
89136339ff
fix(library/init/meta): error message mentions now solve1 instead of focus
2017-06-12 20:42:48 -07:00
Johannes Hölzl
8d438e1012
feat(library/init/meta): add coinduction method
2017-06-12 20:42:48 -07:00
Johannes Hölzl
4368e6b774
fix(library/init/meta): proofs for coinductive predicates introduce now local variable
2017-06-12 20:42:48 -07:00
Johannes Hölzl
b46532bd39
feat(library/init/meta): add error messages when constructing coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
652cbee425
feat(library/init/meta): support nesting for coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
3e6c7efd48
feat(library/init/meta): corec_on for coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
e4d8efc91b
feat(library/init/meta): add attributes and mark parameters and locals as implicit in theorems proveded for coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
f19e1742dd
feat(library/init/meta): produce cases_on for coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
1352d4a5b3
feat(src/frontents/lean): support for coinduction command in frontend
2017-06-12 20:42:48 -07:00
Johannes Hölzl
4d01a6548e
feat(library/init/meta): support mutual coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
23f12a22a2
feat(library/init/meta): add command to construct coinductive predicates
2017-06-12 20:42:48 -07:00
Johannes Hölzl
e88933bac9
feat(library/init/meta/tactic): add tactic.set_env to set environment
2017-06-12 20:42:48 -07:00
Armaël Guéneau
f24932748e
fix(init/meta/interactive): allow dsimp to simplify several hypothesis
2017-06-12 20:37:56 -07:00
Leonardo de Moura
9d5b69ad5c
fix(library/compiler/preprocess): compile_lemma => compile_irrelevant
...
We can also ignore functions that return types at compile_lemma (now
called compile_irrelevant).
fixes #1658
2017-06-12 20:33:31 -07:00
Leonardo de Moura
f5e34f0c02
chore(library): make sure replace_visitor behavior is not compiler dependent, and remove code duplication
2017-06-12 20:18:11 -07:00
Leonardo de Moura
d7e3bd794e
fix(library/equations_compiler): fixes #1663
2017-06-12 19:45:01 -07:00
Sebastian Ullrich
4c5b4fa2f4
chore(.github/PULL_REQUEST_TEMPLATE): typo
2017-06-12 09:56:15 -07:00
Jared Roesch
f3b9db99cf
chore(.github): fix typo
2017-06-12 09:56:15 -07:00
Jared Roesch
47df98aaf0
chore(., .github): move templates to .github
2017-06-12 09:56:15 -07:00
Jared Roesch
5ff6f40897
feat(.): add first pass at contributing & issue & pr templates
2017-06-12 09:56:15 -07:00
Gabriel Ebner
3c0420230f
fix(leanpkg): typo
2017-06-12 17:54:46 +02:00
