cornelis
cornelis copied to clipboard
Allow running load synchronously
Motivation:
You can't really do much of anything else before agda finishes loading a file, so I'd rather my interface freeze to indicate that the buffer is not in a workable state.
Another big motivation is that if we can rely on load being synchronous, we can then write scripts that run load and rely on the load having completed in order to then run other commands afterwards. Concretely, I wanted to have a bind for :CornelisLoad<CR>:CornelisQuestionToMeta<CR>
, but that doesn't currently work out of the box.
Making this PR in a somewhat WIP state since I want to get feedback:
- if you'd accept this
- if this is the way to make a command synchronous
Notably, I'm still not sure this actually makes the command run synchronously, because my example of :CornelisLoad<CR>:CornelisQuestionToMeta<CR>
still doesn't work, but I'm not sure what's going wrong exactly.