From 3a7d9fcafedc4987d0748a8717b2b012a779de39 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 16 Feb 2017 14:14:34 +0100
Subject: [stm] Remove edit_id.

We remove `edit_id` from the STM. In PIDE they serve a different
purpose, however in Coq they were of limited utility and required many
special cases all around the code.

Indeed, parsing is not an asynchronous operation in Coq, thus having
feedback about parsing didn't make much sense. All clients indeed
ignore such feedback and handle parsing in a synchronous way.

XML protocol clients are unaffected, they rely on the instead on the
Fail value.

This commit supersedes PR#203.
---
 lib/feedback.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

(limited to 'lib/feedback.ml')

diff --git a/lib/feedback.ml b/lib/feedback.ml
index 7d9d6bf7f0..df6fe3a629 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -15,9 +15,6 @@ type level =
   | Warning
   | Error
 
-type edit_id = int
-type state_id = Stateid.t
-type edit_or_state_id = Edit of edit_id | State of state_id
 type route_id = int
 
 type feedback_content =
@@ -38,9 +35,9 @@ type feedback_content =
   | Message of level * Loc.t option * Pp.std_ppcmds
 
 type feedback = {
-  id : edit_or_state_id;
+  id       : Stateid.t;
+  route    : route_id;
   contents : feedback_content;
-  route : route_id;
 }
 
 let default_route = 0
@@ -56,7 +53,8 @@ let add_feeder =
 
 let del_feeder fid = Hashtbl.remove feeders fid
 
-let feedback_id    = ref (Edit 0)
+let default_route = 0
+let feedback_id    = ref Stateid.dummy
 let feedback_route = ref default_route
 
 let set_id_for_feedback ?(route=default_route) i =
-- 
cgit v1.2.3