From 6b9b86ccd9f122e684cf4830f3e00bc3f70a0d8a Mon Sep 17 00:00:00 2001 From: Carst Tankink 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.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'lib/feedback.ml') 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; -- cgit v1.2.3