4 files changed, 18 insertions, 0 deletions
diff --git a/lib/feedback.ml b/lib/feedback.ml
index b532c26533..4eb6111576 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -24,6 +24,8 @@ type feedback_content =
   | InProgress of int
   | SlaveStatus of int * string
   | ProcessingInMaster
+  | Goals of Loc.t * string
+  | FileLoaded of string * string
 
 type feedback = {
   id : edit_or_state_id;
@@ -46,6 +48,9 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
   | "slavestatus", [ns] ->
        let n, s = to_pair to_int to_string ns in
        SlaveStatus(n,s)
+  | "goals", [loc;s] -> Goals (to_loc loc, to_string s)
+  | "fileloaded", [dirpath; filename] ->
+       FileLoaded(to_string dirpath, to_string filename)
   | _ -> raise Marshal_error)
 let of_feedback_content = function
   | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
@@ -72,6 +77,12 @@ let of_feedback_content = function
   | SlaveStatus(n,s) ->
       constructor "feedback_content" "slavestatus"
         [of_pair of_int of_string (n,s)]
+  | Goals (loc,s) ->
+      constructor "feedback_content" "goals" [of_loc loc;of_string s]
+  | FileLoaded(dirpath, filename) ->
+      constructor "feedback_content" "fileloaded" [
+        of_string dirpath;
+        of_string filename ]
 
 let of_edit_or_state_id = function
   | Edit id -> ["object","edit"], of_edit_id id
diff --git a/lib/feedback.mli b/lib/feedback.mli
index e7645ca169..c245ec76a1 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -24,6 +24,8 @@ type feedback_content =
   | InProgress of int
   | SlaveStatus of int * string
   | ProcessingInMaster
+  | Goals of Loc.t * string
+  | FileLoaded of string * string
 
 type feedback = {
   id : edit_or_state_id;
diff --git a/lib/flags.ml b/lib/flags.ml
index 36bb447ae9..9dd65db6dc 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -70,6 +70,8 @@ let xml_export = ref false
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
+let feedback_goals = ref false
+
 let time = ref false
 
 let raw_print = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index ea50d41da9..a0ff0f55ea 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -34,6 +34,9 @@ val xml_export : bool ref
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
 
+val feedback_goals : bool ref
+
+
 val time : bool ref
 
 val we_are_parsing : bool ref