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.ml | |
| 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.ml')
| -rw-r--r-- | lib/feedback.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lib/feedback.ml b/lib/feedback.ml index e01844a48..14a1861e8 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -68,6 +68,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 @@ -93,6 +94,7 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with let n, s = to_pair to_string to_string ns in SlaveStatus(n,s) | "goals", [loc;s] -> Goals (to_loc loc, to_string s) + | "structuredgoals", [loc;x]-> StructuredGoals (to_loc loc, x) | "fileloaded", [dirpath; filename] -> FileLoaded(to_string dirpath, to_string filename) | "message", [m] -> Message (to_message m) @@ -124,6 +126,8 @@ let of_feedback_content = function [of_pair of_string of_string (n,s)] | Goals (loc,s) -> constructor "feedback_content" "goals" [of_loc loc;of_string s] + | StructuredGoals (loc, x) -> + constructor "feedback_content" "structuredgoals" [of_loc loc; x] | FileLoaded(dirpath, filename) -> constructor "feedback_content" "fileloaded" [ of_string dirpath; |