Sebastian Ullrich 9d583ab4ec fix: worker: make sure to always report some recent range as progress when waiting (#5428) ... On a document edit, it may be the case that the first nontrivial snapshot is e.g. for a macro-generated tactic call that does not have range information. In that case, instead of just displaying nothing, we should fall back to a previous range, in this case of the original tactic macro.		2024-09-23 15:52:52 +00:00
..
Lean	refactor: split out Lean.Language.Lean.Types (#4881)	2024-07-31 09:50:12 +00:00
Basic.lean	fix: worker: make sure to always report some recent range as progress when waiting (#5428)	2024-09-23 15:52:52 +00:00
Lean.lean	fix: changing whitespace after module header may break subsequent commands (#5312)	2024-09-11 13:00:42 +00:00