aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/queryworkertop.ml
Commit message (Collapse)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* STM: code refactoringGravatar Enrico Tassi2014-11-03
| | | | | This is mainly shuffling code around and removing internal refs that are not needed anymore.
* STM: new worker for queriesGravatar Enrico Tassi2014-10-31
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).