Leonardo de Moura
cfa34dc83e
chore(library): remove workarounds for issue #1682
2017-06-19 16:09:12 -07:00
Leonardo de Moura
ddb6b38d88
fix(frontends/lean/elaborator): fixes #1682
...
@kha Could you please double check whether this is right fix?
2017-06-19 16:04:24 -07:00
Leonardo de Moura
0f64b6088c
chore(frontends/lean): remove then have ... notation
...
This notation was a leftover from Lean 0.1.
2017-06-19 14:20:52 -07:00
Gabriel Ebner
16c6e0ffaf
fix(util/object_serializer): do not compare chars
2017-06-19 20:48:24 +02:00
Gabriel Ebner
b826bdfe43
fix(CMakeLists): force char to be signed
2017-06-19 20:47:57 +02:00
Gabriel Ebner
25a3b13fc7
fix(.travis.yml): move -t0 test to a release configuration
2017-06-19 20:35:11 +02:00
Sebastian Ullrich
91c77680c8
refactor(init/meta/coinductive_predicates,frontends/lean/inductive_cmds): declare coinductive in Lean
2017-06-19 11:27:12 -07:00
Sebastian Ullrich
018ebdd115
feat(frontends/lean/user_command): add user-defined commands
2017-06-19 11:27:12 -07:00
Sebastian Ullrich
606cc85778
chore(library/module): output byte offset of olean corruption
2017-06-19 11:27:12 -07:00
Sebastian Ullrich
4d444b8b18
feat(init/meta/lean/parser): persist environment in tactic_to_parser
2017-06-19 11:27:12 -07:00
Sebastian Ullrich
492cb20438
feat(init/meta/{interactive_base,parser}): decl_attributes, decl_meta_info, parser.set_env
2017-06-19 11:27:12 -07:00
Leonardo de Moura
1fb6c5b211
doc(changes): update
2017-06-19 11:24:17 -07:00
Leonardo de Moura
582aa3338b
fix(frontends/lean): compilation warnings with older versions of gcc
2017-06-19 11:14:22 -07:00
Sebastian Ullrich
95b317fa64
refactor(frontends/lean): do not hard code commands accepting attributes & modifiers
2017-06-19 11:09:26 -07:00
Gabriel Ebner
2e142d87ae
fix(library/init/data/repr): give correct implementation of nat.repr
2017-06-19 16:20:27 +02:00
Gabriel Ebner
82bb37422d
fix(library/init/data/int): add to_string instance for integers
2017-06-19 14:30:58 +02:00
Gabriel Ebner
981f439de5
chore(gitignore): ignore nix files
2017-06-19 13:16:04 +02:00
Gabriel Ebner
856a88833f
fix(util/debug,util/serializer): use basic_ios::eof to check for end-of-file
2017-06-19 13:04:06 +02:00
Gabriel Ebner
95f8a50a03
fix(frontends/lean/scanner): use platform-independent end-of-file marker
2017-06-19 10:39:08 +02:00
Leonardo de Moura
75ec32de94
doc(changes): has_repr and has_to_string
2017-06-18 18:40:29 -07:00
Leonardo de Moura
2866607319
chore(tests): fix tests
2017-06-18 18:33:38 -07:00
Leonardo de Moura
b8fa7f5311
fix(library): expr, level, hash_map, rb_map has_repr instances should be has_to_string since they do not produce results that can be parsed by Lean
...
See #1664
2017-06-18 18:33:27 -07:00
Leonardo de Moura
049fecee23
fix(library/init): name has_repr instance is actually a has_to_string instance
...
See #1664
2017-06-18 18:33:16 -07:00
Leonardo de Moura
8b88f21c91
refactor(library): add has_to_string back (but it produces unquoted values)
...
See issue #1664
2017-06-18 18:30:10 -07:00
Leonardo de Moura
dc1a1c8540
refactor(library): has_to_string ==> has_repr
...
See issue #1664
This is just the first step to implement proposal described at issue #1664 .
2017-06-18 18:29:19 -07:00
Leonardo de Moura
c33fd8b0fd
fix(frontends/lean/elaborator): fixes #1669
2017-06-18 16:14:48 -07:00
Leonardo de Moura
0996a606d1
chore(.travis.yml): save result of .travis.yml.in
2017-06-18 16:10:49 -07:00
Leonardo de Moura
fb24cc9957
chore(.travis.yml.in): fix release upload
...
@gebner Is this the change you meant in the slack channel?
2017-06-18 11:53:01 -07:00
Leonardo de Moura
3ea5ac4340
chore(*): update change log, and bump work in progress version to 3.2.1
2017-06-18 11:15:09 -07:00
Leonardo de Moura
9a386ae188
chore(*): version 3.2.0
2017-06-18 10:40:13 -07:00
Daniel Selsam
cda196f278
perf(library/delayed_abstraction.cpp): stack caches when pushing delayed abstractions
2017-06-18 10:24:20 -07:00
Gabriel Ebner
c9aacf396e
fix(emacs/lean-hole): fix end position computation
...
@leodemoura The problem with holes at the end of a file is now fixed.
2017-06-18 08:08:40 +02:00
Sebastian Ullrich
d994da97c1
chore(doc/changes): fix link
2017-06-16 16:17:25 +02:00
David Christiansen
550f8bcacb
fix(emacs): Improve cursor motion with output boxes
...
Part of making cursor motion consistent was getting rid of the
versions that float to the right. So now all command output is just
under the command.
2017-06-16 12:39:52 +02:00
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
