Gabriel Ebner
|
f16c2c68db
|
perf(emacs/lean-server): speed up task overlays
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
83c4b410be
|
feat(emacs/lean-server): more awesome fringe highlighting
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
7442aa0752
|
fix(frontends/lean/parser): better task description
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
24e19bdd00
|
feat(emacs): add tooltip to task overlays
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
af588add56
|
fix(emacs/lean-server): correctly react to scrolling
|
2017-03-24 07:22:28 +01:00 |
|
Gabriel Ebner
|
34586a2e82
|
feat(util/log_tree): deindent _next nodes
|
2017-03-24 07:04:35 +01:00 |
|
Gabriel Ebner
|
fdd80c12dd
|
feat(util/log_tree): inherit description
|
2017-03-24 07:04:35 +01:00 |
|
Gabriel Ebner
|
c55579dd69
|
fix(frontends/lean/scanner): initialize m_pos
|
2017-03-24 07:04:35 +01:00 |
|
Leonardo de Moura
|
7543d9e050
|
chore(tests/lean/io_fs_error): fix test
|
2017-03-23 18:52:37 -07:00 |
|
Leonardo de Moura
|
8cf43e1b30
|
feat(library/tactic/tactic_state): add tactic.run_io
|
2017-03-23 18:17:53 -07:00 |
|
Leonardo de Moura
|
7db44ce403
|
chore(library/vm/vm_io): style
|
2017-03-23 16:58:28 -07:00 |
|
Leonardo de Moura
|
fe3875a103
|
feat(library/system/io): add stdin, stdout and stderr
|
2017-03-23 16:49:39 -07:00 |
|
Leonardo de Moura
|
82748a61b7
|
feat(library/system/io): basic file system API
|
2017-03-23 16:30:16 -07:00 |
|
Leonardo de Moura
|
527c8851a8
|
refactor(library/system/io): use type classes
|
2017-03-23 14:29:07 -07:00 |
|
Leonardo de Moura
|
ccd9a8212a
|
chore(shell/lean_js): compilation warning
|
2017-03-23 12:56:35 -07:00 |
|
Gabriel Ebner
|
0d4f829ada
|
fix(library/mt_task_queue): fix abort
|
2017-03-23 15:37:52 +01:00 |
|
Gabriel Ebner
|
8814fe8276
|
chore(tests/lean): add test for error position clamping
|
2017-03-23 09:23:57 +01:00 |
|
Gabriel Ebner
|
69322cd523
|
fix(util/task): evaluate dependencies iteratively
|
2017-03-23 09:16:49 +01:00 |
|
Gabriel Ebner
|
2da9d72491
|
chore(tests/lean/interactive): fix test
|
2017-03-23 09:14:32 +01:00 |
|
Gabriel Ebner
|
73826eee54
|
chore(util/rb_tree): fix clang warning
|
2017-03-23 09:07:50 +01:00 |
|
Gabriel Ebner
|
14c24a66a1
|
feat(emacs): provide commands to change check mode
|
2017-03-23 09:07:09 +01:00 |
|
Gabriel Ebner
|
a6f7f31e85
|
refactor(shell,emacs): handle different checking modes in server
|
2017-03-23 09:07:09 +01:00 |
|
Sebastian Ullrich
|
1f07319bc7
|
fix(emacs/lean-server): Emacs 24 compatibility
|
2017-03-23 09:07:09 +01:00 |
|
Gabriel Ebner
|
a8ba78e20a
|
refactor(frontends/lean/tactic_notation): remove irtactic in favor of itactic
|
2017-03-23 09:07:08 +01:00 |
|
Gabriel Ebner
|
d90dda01b0
|
chore(*): fix tests
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
9dfd8e1018
|
fix(shell/server): fix field completion
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
5e29fe227e
|
fix(shell/server): set global ios in info and complete tasks
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
dfb5dad1a3
|
chore(util/log_tree): style
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
c7ca21625c
|
feat(util/log_tree): annotate nodes with detail levels
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
ef0e113b4b
|
chore(tests): fix tests
|
2017-03-23 09:03:43 +01:00 |
|
Gabriel Ebner
|
0853d9fd2a
|
fix(util/thread): fix single-threaded build
|
2017-03-23 09:03:42 +01:00 |
|
Gabriel Ebner
|
05c151c60e
|
fix(CMakeLists): make leanchecker link to jemalloc
|
2017-03-23 09:03:42 +01:00 |
|
Gabriel Ebner
|
098d6f8f2a
|
refactor(init/meta/tactic): remove report_errors argument from to_expr
|
2017-03-23 09:03:42 +01:00 |
|
Gabriel Ebner
|
c8fff9f4ff
|
refactor(init/meta/interaction_monad): replace rstep by istep
|
2017-03-23 09:03:41 +01:00 |
|
Gabriel Ebner
|
7f1569535b
|
feat(library/messages): clamp message position to current location
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
98f86ccabd
|
chore(frontends/lean/parser): remove obsolete option
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
e64c10dd20
|
feat(emacs): create all info buffers by default
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
e35968cda1
|
feat(util/memory): implement get_current_rss using the jemalloc API
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
c5c0a74d77
|
fix(frontends/lean/definition_cmds): reinstate fallback to sorry
|
2017-03-23 09:01:00 +01:00 |
|
Gabriel Ebner
|
a591e35544
|
chore(*): fix tests
|
2017-03-23 09:00:59 +01:00 |
|
Gabriel Ebner
|
27f6f2a951
|
perf(util/log_tree): do not traverse the whole tree every time
|
2017-03-23 09:00:59 +01:00 |
|
Gabriel Ebner
|
feb13c47f8
|
perf(util/task_builder): speed up traverse
|
2017-03-23 09:00:59 +01:00 |
|
Gabriel Ebner
|
7036bec999
|
fix(util/cancellable): fix quadratic runtime with many children
|
2017-03-23 09:00:59 +01:00 |
|
Gabriel Ebner
|
d26e870aa5
|
chore(*): fix tests
|
2017-03-23 09:00:59 +01:00 |
|
Gabriel Ebner
|
cfa0f798ac
|
fix(util/log_tree): fix memory leak
|
2017-03-23 09:00:59 +01:00 |
|
Gabriel Ebner
|
677bf43da3
|
fix(library): fix various leaks
|
2017-03-23 09:00:59 +01:00 |
|
Gabriel Ebner
|
796097ec31
|
fix(util/log_tree): fix reference cycle between log_tree and tasks
|
2017-03-23 09:00:59 +01:00 |
|
Gabriel Ebner
|
3c515cc772
|
refactor(util/log_tree): use for_each
|
2017-03-23 09:00:59 +01:00 |
|
Gabriel Ebner
|
b6e79d646d
|
fix(util/cancellable): actually set interrupt flag
|
2017-03-23 09:00:59 +01:00 |
|
Gabriel Ebner
|
d0cc6f16b1
|
fix(shell/server): remove cancellation token from snapshot
|
2017-03-23 09:00:59 +01:00 |
|