From cfb5201e2ebc2516e3de7c578355db8bd4f08d35 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 31 Oct 2014 15:43:08 +0100
Subject: Feedback message: hold extra info to help routing

PIDE based GUIs can take advantage of multiple panels and get
some feedback routed there. E.g. query panel
---
 intf/vernacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 0286687466..5cd34038f6 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -458,7 +458,7 @@ type vernac_type =
   | VtQuery of vernac_part_of_script * report_with
   | VtStm of vernac_control * vernac_part_of_script
   | VtUnknown
-and report_with = Stateid.t (* report feedback on a different id *)
+and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *)
 and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *)
 and vernac_start = string * opacity_guarantee * Id.t list
 and vernac_sideff_type = Id.t list
-- 
cgit v1.2.3