From 4ed9c7ad75a7f09d723bdfce6f7dd086c60e0601 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 16 Feb 2017 22:31:13 +0100
Subject: [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.
---
 dev/doc/changes.txt | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'dev')

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 =
 =========================================
-- 
cgit v1.2.3


From ce2b2058587224ade9261cd4127ef4f6e94d356b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 27 Feb 2017 20:16:40 +0100
Subject: [stm] Port the toplevel to the STM.

- We clean-up `Vernac` and make it use the STM API.

- Now functions in `Vernac` for use in the toplevel and compiler take
  an starting `Stateid.t`.

- Duplicated `Stm.interp` entry point is removed.

- The XML protocol call `interp` is disabled.
---
 dev/doc/changes.txt | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 30edea7f2f..7e7bb98580 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -156,6 +156,19 @@ document type". This allows for a more uniform handling of printing
 
 - A few unused hooks were removed due to cleanups, no clients known.
 
+** Toplevel and Vernacular API **
+
+- The components related to vernacular interpretation have been moved
+  to their own folder `vernac/` whereas toplevel now contains the
+  proper toplevel shell and compiler.
+
+- Coq's toplevel has been ported to directly use the common `Stm`
+  API. The signature of a few functions has changed as a result.
+
+** XML Protocol **
+
+- The legacy `interp` call has been turned into a noop.
+
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
 =========================================
-- 
cgit v1.2.3


From 2f0a56562112c4bd66082fb3eafffb8cf6f03a88 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 29 Mar 2017 17:47:06 +0200
Subject: [stm] Improve error messages on add/parse.

As suggested by @psteckler in #524 , we give more explicit information
about what is wrong.

We also provide some debug information for the possible dangerous case
of having the tip go out of sync with the real installed state (which
will make parsing fail if there was some changes to the parser).

We also fix a couple of typos noticed by Paul, thanks Paul.
---
 dev/doc/changes.txt | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index 7e7bb98580..fe0b587b11 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -148,7 +148,7 @@ document type". This allows for a more uniform handling of printing
 
 - 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.
+  either succeed or raise an exception.
 
 - `Feedback` is now only emitted for asynchronous operations. As a
   consequence, it always carries a valid stateid and the type has
@@ -167,7 +167,7 @@ document type". This allows for a more uniform handling of printing
 
 ** XML Protocol **
 
-- The legacy `interp` call has been turned into a noop.
+- The legacy `Interp` call has been turned into a noop.
 
 =========================================
 = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 =
-- 
cgit v1.2.3