diff options
| author |  Carst Tankink <carst.tankink@inria.fr> | 2014-09-30 14:44:53 +0200 |
|---|---|---|
| committer |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-10-01 18:08:51 +0200 |
| commit | 6b9b86ccd9f122e684cf4830f3e00bc3f70a0d8a (patch) | |
| tree | 9720f305bab09a6cfa2cfafcc7b21d680e7ddb79 /lib/feedback.mli | |
| parent | 9a3abe5b18a84733c0c01c2647108196798a761c (diff) | |
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.
Diffstat (limited to 'lib/feedback.mli')
| -rw-r--r-- | lib/feedback.mli | 1 |
1 files changed, 1 insertions, 0 deletions
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 |