Sebastian Ullrich
|
1f601708e4
|
fix: print messages to stderr
This ensures that errors during dependency resolution in the Makefile actually show up
|
2019-11-10 09:01:43 -08:00 |
|
Sebastian Ullrich
|
64ab576dbf
|
fix(shell/lean,library/messages): print messages in correct order (and immediately) when --json was not given
|
2019-02-01 17:10:14 +01:00 |
|
Sebastian Ullrich
|
904d7c4a88
|
chore(*): remove old task API and task queues
|
2018-09-11 13:55:25 -07:00 |
|
Sebastian Ullrich
|
af55cb13e7
|
fix(library/messages,library/init/lean/message): wrap message_log in structure, reverse in the end
|
2018-09-11 13:55:25 -07:00 |
|
Sebastian Ullrich
|
99ab0e9d67
|
refactor(library/messages): make an object_ref
|
2018-09-11 13:55:25 -07:00 |
|
Leonardo de Moura
|
78f4edaf57
|
chore(frontends/lean): remove info_manager and interactive modules
|
2018-09-04 17:22:16 -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 |
|
Sebastian Ullrich
|
4a33045b84
|
chore(tests/lean,shell/lean): run leantests and leanruntests in parallel
|
2017-03-30 06:04:00 +02:00 |
|
Gabriel Ebner
|
7f1569535b
|
feat(library/messages): clamp message position to current location
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
bbe30e1bc5
|
feat(library/module): only report sorry once per declaration
|
2017-03-23 08:57:56 +01:00 |
|
Gabriel Ebner
|
5f872912e0
|
refactor(shell/lean): set exit status 1 iff at least one error was reported
|
2017-03-23 08:57:56 +01:00 |
|
Gabriel Ebner
|
595cbb8fe9
|
refactor(*): task<T>, log_tree, cancellation_token
|
2017-03-23 08:57:52 +01:00 |
|
Sebastian Ullrich
|
9d8c84713c
|
refactor(*): reduce exception context info from expr to pos_info
|
2017-02-17 13:45:57 +01:00 |
|
Gabriel Ebner
|
a8df381d20
|
feat(*): parallel compilation
|
2016-11-29 11:12:40 -08:00 |
|
Gabriel Ebner
|
66be9c31db
|
refactor(library/flycheck): use flycheck_message_stream instead of option
|
2016-10-13 18:49:10 -07:00 |
|
Gabriel Ebner
|
b05b514cc2
|
refactor(*): structured message objects
|
2016-10-13 18:49:10 -07:00 |
|