diff options
| author | Emilio Jesus Gallego Arias | 2017-02-16 22:31:13 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-12 16:29:11 +0200 |
| commit | 4ed9c7ad75a7f09d723bdfce6f7dd086c60e0601 (patch) | |
| tree | d322952b91456f1f2811d7758fd8fef690405577 /dev | |
| parent | 3a7d9fcafedc4987d0748a8717b2b012a779de39 (diff) | |
[stm] Move main parsing entry point to the STM.
Mainly due to notations, proof modes and plugins, parsing in Coq is
stateful, so we expose a state-aware parsing API in the STM.
This is a first move to unify all the parsing entry points in the Stm
and the toplevel, and allows STM clients to control their input stream
properly. This greatly helps for instance, with whole-document
parsing.
This commit supersedes PR#204.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index af077bbb40..30edea7f2f 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -139,6 +139,23 @@ document type". This allows for a more uniform handling of printing module Tag +** Stm API ** + +- We have streamlined the `Stm` API, now `add` and `query` take a + `coq_parsable` instead a `string` so clients can have more control + over their input stream. As a consequence, their types have been + modified. + +- The main parsing entry point has also been moved to the + `Stm`. Parsing is considered a synchronous operation so it will + either succeed of emit an exception. + +- `Feedback` is now only emitted for asynchronous operations. As a + consequence, it always carries a valid stateid and the type has + changed to accommodate that. + +- A few unused hooks were removed due to cleanups, no clients known. + ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= |