4 files changed, 29 insertions, 1 deletions
diff --git a/lib/clib.mllib b/lib/clib.mllib
index 9667df31c4..a9b596b99e 100644
--- a/lib/clib.mllib
+++ b/lib/clib.mllib
@@ -15,6 +15,7 @@ CList
 CString
 CArray
 Util
+Loc
 Serialize
 Xml_utils
 Flags
diff --git a/lib/interface.mli b/lib/interface.mli
index 3ff05f6f2e..e1419da9bf 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -123,6 +123,7 @@ type edit_id = int
 type feedback_content =
   | AddedAxiom
   | Processed
+  | GlobRef of Loc.t * string * string * string * string
 
 type feedback = {
   edit_id : edit_id;
diff --git a/lib/lib.mllib b/lib/lib.mllib
index eb7285bdda..eabac2cfd8 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -1,6 +1,5 @@
 Xml_lexer
 Xml_parser
-Loc
 Errors
 Bigint
 Dyn
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 823f4245d5..186c3dc890 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -525,15 +525,42 @@ let is_message = function
 | Element ("message", _, _) -> true
 | _ -> false
 
+let of_loc loc =
+  let start, stop = Loc.unloc loc in
+  Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[])
+
+let to_loc xml = match xml with
+| Element ("loc", l,[]) ->
+    (try
+      let start = List.assoc "start" l in
+      let stop = List.assoc "stop" l in
+      Loc.make_loc (int_of_string start, int_of_string stop)
+    with Not_found | Invalid_argument _ -> raise Marshal_error)
+| _ -> raise Marshal_error
+
 let to_feedback_content xml = do_match xml "feedback_content"
   (fun s args -> match s with
   | "addedaxiom" -> AddedAxiom
   | "processed" -> Processed
+  | "globref" ->
+       (match args with
+       | [loc; filepath; modpath; ident; ty] ->
+            GlobRef(to_loc loc, to_string filepath, to_string modpath,
+                    to_string ident, to_string ty)
+       | _ -> raise Marshal_error)
   | _ -> raise Marshal_error)
 
 let of_feedback_content = function
 | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
 | Processed -> constructor "feedback_content" "processed" []
+| GlobRef(loc, filepath, modpath, ident, ty) ->
+    constructor "feedback_content" "globref" [
+      of_loc loc;
+      of_string filepath;
+      of_string modpath;
+      of_string ident;
+      of_string ty
+    ]
 
 let of_feedback msg =
   let content = of_feedback_content msg.content in