| Commit message (Collapse) | Author | Age |
|
|
|
| |
4.02.3 has been the minimal OCaml version for a while now.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We make the Stm API functional over an opaque `doc` type. This allows
to have a much better picture of what the toplevel is doing; now
almost all users of STM private data are marked by typing.
For now only, the API is functional; a PR switching the internals
should come soon thou; however we must first fix some initialization
bugs.
Due to some users, we modify `feedback` internally to include a
"document id" field; we don't expose this change in the IDE protocol
yet.
|
| |
|
|
|
|
|
| |
This is a small, but convenient refactoring, as it will allow common
argument parsing.
|
| |
|
| |
|
|
|
|
|
| |
This is mainly shuffling code around and removing internal
refs that are not needed anymore.
|
|
With the options -async-queries-always-delegate queries are
always delegated to a worker process (Eval, Check, ...).
Users of PIDE based UIs (in Denmark) reported that the current
behavior of processing query synchronously is rather unexpected
when one is used to get proofs processed asynchronously.
Non instantaneous queries are part of many scripts and are there
as "tests" for testing the execution of recursive functions.
A standard proof script shape in an ongoing work by Appel and Bengtson
is made of blocks like:
- recursive function definition,
- some tests,
- some proofs
And one cannot quickly jump over the tests (only the proofs).
Enclosing the queries into dummy proofs to recover a reactive UI
is just annoying. Hence this patch.
Currently CoqIDE is not able to integrate the asynchronous feedback
of the query workers into the document, hence if one passes the option
to CoqIDE one only gets a boolean out of queries (processed/error).
|