From 6b9b86ccd9f122e684cf4830f3e00bc3f70a0d8a Mon Sep 17 00:00:00 2001
From: Carst Tankink <carst.tankink@inria.fr>
Date: Tue, 30 Sep 2014 14:44:53 +0200
Subject: STM: report the (structured) goals as XML

The leafs of the XML trees are still pretty-printed strings, but this
could be refined later on.
---
 lib/feedback.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib/feedback.mli')

diff --git a/lib/feedback.mli b/lib/feedback.mli
index 7e7b57625..775f71e9e 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -43,6 +43,7 @@ type feedback_content =
   | SlaveStatus of string * string
   | ProcessingInMaster
   | Goals of Loc.t * string
+  | StructuredGoals of Loc.t * xml
   | FileLoaded of string * string
   | Message of message
 
-- 
cgit v1.2.3