[location] Remove Loc.ghost.

Now it is a private field, locations are optional.

5 files changed, 240 insertions, 241 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 222b9eed9..7825fb45e 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -465,20 +465,22 @@ object(self)
           self#attach_tooltip ~loc sentence
             (Printf.sprintf "%s %s %s" filepath ident ty)
       | Message(Error, loc, msg), Some (id,sentence) ->
-          let uloc = Option.default Loc.ghost loc in
           log_pp ?id Pp.(str "ErrorMsg" ++ msg);
           remove_flag sentence `PROCESSING;
           let rmsg = Pp.string_of_ppcmds msg     in
-          add_flag sentence (`ERROR (uloc, rmsg));
+          Option.iter (fun loc ->
+              add_flag sentence (`ERROR (loc, rmsg));
+            ) loc;
           self#mark_as_needed sentence;
-          self#attach_tooltip sentence ?loc rmsg;
+          self#attach_tooltip ?loc sentence rmsg;
           self#position_tag_at_sentence ?loc Tags.Script.error sentence
       | Message(Warning, loc, msg), Some (id,sentence) ->
-          let uloc = Option.default Loc.ghost loc in
           log_pp ?id Pp.(str "WarningMsg" ++ msg);
           let rmsg = Pp.string_of_ppcmds msg     in
-          add_flag sentence (`WARNING (uloc, rmsg));
-          self#attach_tooltip sentence ?loc rmsg;
+          Option.iter (fun loc ->
+              add_flag sentence (`WARNING (loc, rmsg));
+            ) loc;
+          self#attach_tooltip ?loc sentence rmsg;
           self#position_tag_at_sentence ?loc Tags.Script.warning sentence;
           messages#push Warning msg
       | Message(lvl, loc, msg), Some (id,sentence) ->
@@ -528,14 +530,14 @@ object(self)
     let start, stop, phrase = self#get_sentence sentence in
     self#position_tag_at_iter ?loc start stop tag phrase
 
-  method private process_interp_error queue sentence loc msg tip id =
+  method private process_interp_error ?loc queue sentence msg tip id =
     Coq.bind (Coq.return ()) (function () ->
     let start, stop, phrase = self#get_sentence sentence in
     buffer#remove_tag Tags.Script.to_process ~start ~stop;
     self#discard_command_queue queue;
     pop_info ();
     if Stateid.equal id tip || Stateid.equal id Stateid.dummy then begin
-      self#position_tag_at_iter ~loc start stop Tags.Script.error phrase;
+      self#position_tag_at_iter ?loc start stop Tags.Script.error phrase;
       buffer#place_cursor ~where:stop;
       messages#clear;
       messages#push Feedback.Error msg;
@@ -649,9 +651,9 @@ object(self)
                   if Queue.is_empty queue then loop tip []
                   else loop tip (List.rev topstack)
               | Fail (id, loc, msg) ->
-                  let loc = Option.cata Loc.make_loc Loc.ghost loc in
+                  let loc = Option.map Loc.make_loc loc in
                   let sentence = Doc.pop document in
-                  self#process_interp_error queue sentence loc msg tip id in
+                  self#process_interp_error ?loc queue sentence msg tip id in
             Coq.bind coq_query handle_answer
       in
       let tip =
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index bf86db08f..7f30a4acc 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -390,8 +390,8 @@ let quit = ref false
 (** Serializes the output of Stm.get_ast  *)
 let print_ast id =
   match Stm.get_ast id with
-  | Some (expr, loc) -> begin
-      try  Texmacspp.tmpp expr loc
+  | Some (loc, expr) -> begin
+      try  Texmacspp.tmpp ~loc expr
       with e -> Xml_datatype.PCData ("ERROR " ^ Printexc.to_string e)
     end
   | None     -> Xml_datatype.PCData "ERROR"
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index f86b260df..0a07a830b 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -17,12 +17,12 @@ open Extend
 open Libnames
 open Constrexpr_ops
 
-let unlock loc =
-  let start, stop = Loc.unloc loc in
+let unlock ?loc =
+  let start, stop = Option.cata Loc.unloc (0,0) loc in
   (string_of_int start, string_of_int stop)
 
-let xmlWithLoc loc ename attr xml =
-  let start, stop = unlock loc in
+let xmlWithLoc ?loc ename attr xml =
+  let start, stop = unlock ?loc in
   Element(ename, [ "begin", start; "end", stop ] @ attr, xml)
 
 let get_fst_attr_in_xml_list attr xml_list =
@@ -49,32 +49,32 @@ let compare_begin_att xml1 xml2 =
   | (_, s1), (_, s2) when int_of_string s1 < int_of_string s2 -> -1
   | _ -> 0
 
-let xmlBeginSection loc name = xmlWithLoc loc "beginsection" ["name", name] []
+let xmlBeginSection ?loc name = xmlWithLoc ?loc "beginsection" ["name", name] []
 
-let xmlEndSegment loc name = xmlWithLoc loc "endsegment" ["name", name] []
+let xmlEndSegment ?loc name = xmlWithLoc ?loc "endsegment" ["name", name] []
 
-let xmlThm typ name loc xml =
-  xmlWithLoc loc "theorem" ["type", typ; "name", name] xml
+let xmlThm ?loc typ name xml =
+  xmlWithLoc ?loc "theorem" ["type", typ; "name", name] xml
 
-let xmlDef typ name loc xml =
-  xmlWithLoc loc "definition" ["type", typ; "name", name] xml
+let xmlDef ?loc typ name xml =
+  xmlWithLoc ?loc "definition" ["type", typ; "name", name] xml
 
-let xmlNotation attr name loc xml =
-  xmlWithLoc loc "notation" (("name", name) :: attr) xml
+let xmlNotation ?loc attr name xml =
+  xmlWithLoc ?loc "notation" (("name", name) :: attr) xml
 
-let xmlReservedNotation attr name loc =
-  xmlWithLoc loc "reservednotation" (("name", name) :: attr) []
+let xmlReservedNotation ?loc attr name =
+  xmlWithLoc ?loc "reservednotation" (("name", name) :: attr) []
 
-let xmlCst name ?(attr=[]) loc =
-  xmlWithLoc loc "constant" (("name", name) :: attr) []
+let xmlCst ?loc ?(attr=[]) name =
+  xmlWithLoc ?loc "constant" (("name", name) :: attr) []
 
-let xmlOperator name ?(attr=[]) ?(pprules=[]) loc =
-  xmlWithLoc loc "operator"
+let xmlOperator ?loc ?(attr=[]) ?(pprules=[]) name =
+  xmlWithLoc ?loc "operator"
     (("name", name) :: List.map (fun (a,b) -> "format"^a,b) pprules @ attr) []
 
-let xmlApply loc ?(attr=[]) xml = xmlWithLoc loc "apply" attr xml
+let xmlApply ?loc ?(attr=[]) xml = xmlWithLoc ?loc "apply" attr xml
 
-let xmlToken loc ?(attr=[]) xml = xmlWithLoc loc "token" attr xml
+let xmlToken ?loc ?(attr=[]) xml = xmlWithLoc ?loc "token" attr xml
 
 let xmlTyped xml = Element("typed", (backstep_loc xml), xml)
 
@@ -88,23 +88,23 @@ let xmlWith xml = Element("with", [], xml)
 
 let xmlAssign id xml = Element("assign", ["target",string_of_id id], [xml])
 
-let xmlInductive kind loc xml = xmlWithLoc loc "inductive" ["kind",kind] xml
+let xmlInductive ?loc kind xml = xmlWithLoc ?loc "inductive" ["kind",kind] xml
 
 let xmlCoFixpoint xml = Element("cofixpoint", [], xml)
 
 let xmlFixpoint xml = Element("fixpoint", [], xml)
 
-let xmlCheck loc xml = xmlWithLoc loc "check" [] xml
+let xmlCheck ?loc xml = xmlWithLoc ?loc "check" [] xml
 
-let xmlAssumption kind loc xml = xmlWithLoc loc "assumption" ["kind",kind] xml
+let xmlAssumption ?loc kind xml = xmlWithLoc ?loc "assumption" ["kind",kind] xml
 
-let xmlComment loc xml = xmlWithLoc loc "comment" [] xml
+let xmlComment ?loc xml = xmlWithLoc ?loc "comment" [] xml
 
-let xmlCanonicalStructure attr loc = xmlWithLoc loc "canonicalstructure" attr []
+let xmlCanonicalStructure ?loc attr = xmlWithLoc ?loc "canonicalstructure" attr []
 
-let xmlQed ?(attr=[]) loc = xmlWithLoc loc "qed" attr []
+let xmlQed ?loc ?(attr=[]) = xmlWithLoc ?loc "qed" attr []
 
-let xmlPatvar id loc = xmlWithLoc loc "patvar" ["id", id] []
+let xmlPatvar ?loc id = xmlWithLoc ?loc "patvar" ["id", id] []
 
 let xmlReference ref =
   let name = Libnames.string_of_reference ref in
@@ -112,38 +112,38 @@ let xmlReference ref =
   let b, e = string_of_int i, string_of_int j in
   Element("reference",["name", name; "begin", b; "end", e] ,[])
 
-let xmlRequire loc ?(attr=[]) xml = xmlWithLoc loc "require" attr xml
-let xmlImport loc ?(attr=[]) xml = xmlWithLoc loc "import" attr xml
+let xmlRequire ?loc ?(attr=[]) xml = xmlWithLoc ?loc "require" attr xml
+let xmlImport ?loc ?(attr=[]) xml = xmlWithLoc ?loc "import" attr xml
 
-let xmlAddLoadPath loc ?(attr=[]) xml = xmlWithLoc loc "addloadpath" attr xml
-let xmlRemoveLoadPath loc ?(attr=[]) = xmlWithLoc loc "removeloadpath" attr
-let xmlAddMLPath loc ?(attr=[]) = xmlWithLoc loc "addmlpath" attr
+let xmlAddLoadPath ?loc ?(attr=[]) xml = xmlWithLoc ?loc "addloadpath" attr xml
+let xmlRemoveLoadPath ?loc ?(attr=[]) = xmlWithLoc ?loc "removeloadpath" attr
+let xmlAddMLPath ?loc ?(attr=[]) = xmlWithLoc ?loc "addmlpath" attr
 
-let xmlExtend loc xml = xmlWithLoc loc "extend" [] xml
+let xmlExtend ?loc xml = xmlWithLoc ?loc "extend" [] xml
 
-let xmlScope loc action ?(attr=[]) name xml =
-  xmlWithLoc loc "scope" (["name",name;"action",action] @ attr) xml
+let xmlScope ?loc ?(attr=[]) action name xml =
+  xmlWithLoc ?loc "scope" (["name",name;"action",action] @ attr) xml
 
-let xmlProofMode loc name = xmlWithLoc loc "proofmode" ["name",name] []
+let xmlProofMode ?loc name = xmlWithLoc ?loc "proofmode" ["name",name] []
 
-let xmlProof loc xml = xmlWithLoc loc "proof" [] xml
+let xmlProof ?loc xml = xmlWithLoc ?loc "proof" [] xml
 
 let xmlSectionSubsetDescr name ssd =
   Element("sectionsubsetdescr",["name",name],
     [PCData (Proof_using.to_string ssd)])
 
-let xmlDeclareMLModule loc s =
-  xmlWithLoc loc "declarexmlmodule" []
+let xmlDeclareMLModule ?loc s =
+  xmlWithLoc ?loc "declarexmlmodule" []
     (List.map (fun x -> Element("path",["value",x],[])) s)
 
 (* tactics *)
-let xmlLtac loc xml = xmlWithLoc loc "ltac" [] xml
+let xmlLtac ?loc xml = xmlWithLoc ?loc "ltac" [] xml
 
 (* toplevel commands *)
-let xmlGallina loc xml = xmlWithLoc loc "gallina" [] xml
+let xmlGallina ?loc xml = xmlWithLoc ?loc "gallina" [] xml
 
-let xmlTODO loc x =
-  xmlWithLoc loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+let xmlTODO ?loc x =
+  xmlWithLoc ?loc "todo" [] [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
 
 let string_of_name n =
   match n with
@@ -189,7 +189,7 @@ match sm with
   | SetOnlyParsing -> ["onlyparsing", ""]
   | SetCompatVersion v -> ["compat", Flags.pr_version v]
   | SetFormat (system, (loc, s)) ->
-      let start, stop = unlock loc in
+      let start, stop = unlock ~loc in
       ["format-"^system, s; "begin", start; "end", stop]
 
 let string_of_assumption_kind l a many =
@@ -217,7 +217,7 @@ let rec pp_bindlist bl =
             let names =
               (List.map
                 (fun (loc, name) ->
-                  xmlCst (string_of_name name) loc) loc_names) in
+                  xmlCst ~loc (string_of_name name)) loc_names) in
             match e with
               | _, CHole _ -> names
               | _ -> names @ [pp_expr e])
@@ -237,13 +237,13 @@ and pp_local_binder lb = (* don't know what it is for now *)
       pp_expr ~attr:attrs value
   | CLocalAssum (namll, _, ce) ->
       let ppl =
-        List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in
+        List.map (fun (loc, nam) -> (xmlCst ~loc (string_of_name nam))) namll in
       xmlTyped (ppl @ [pp_expr ce])
   | CLocalPattern _ ->
       assert false
 and pp_local_decl_expr lde = (* don't know what it is for now *)
   match lde with
-  | AssumExpr (_, ce) -> pp_expr ce
+  | AssumExpr (_, ce)  -> pp_expr ce
   | DefExpr (_, ce, _) -> pp_expr ce
 and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
   (* inductive_expr *)
@@ -265,7 +265,7 @@ and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
     match optid with
     | None -> []
     | Some (loc, id) ->
-        let start, stop = unlock loc in
+        let start, stop = unlock ~loc in
         ["begin", start; "end", stop ; "name", Id.to_string id] in
   let kind, expr =
     match roe with
@@ -276,7 +276,7 @@ and pp_recursion_order_expr optid roe = (* don't know what it is for now *)
   Element ("recursion_order", ["kind", kind] @ attrs, expr)
 and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
   (* fixpoint_expr *)
-  let start, stop = unlock loc in
+  let start, stop = unlock ~loc in
   let id = Id.to_string id in
   [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
   (* fixpoint name *)
@@ -290,7 +290,7 @@ and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) =
 and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
   (* Nota: it is like fixpoint_expr without (optid, roe)
    * so could be merged if there is no more differences *)
-  let start, stop = unlock loc in
+  let start, stop = unlock ~loc in
   let id = Id.to_string id in
   [Element ("lident", ["begin", start; "end", stop ; "name", id], [])] @
   (* cofixpoint name *)
@@ -300,37 +300,37 @@ and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
   | Some ce -> [pp_expr ce]
   | None -> []
   end
-and pp_lident (loc, id) = xmlCst (Id.to_string id) loc
+and pp_lident (loc, id) = xmlCst ~loc (Id.to_string id)
 and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
 and pp_cases_pattern_expr (loc, cpe) =
   match cpe with
   | CPatAlias (cpe, id) ->
-      xmlApply loc
-        (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
+      xmlApply ~loc
+        (xmlOperator ~loc ~attr:["name", string_of_id id] "alias" ::
           [pp_cases_pattern_expr cpe])
   | CPatCstr (ref, None, cpel2) ->
-      xmlApply loc
-        (xmlOperator "reference"
-           ~attr:["name", Libnames.string_of_reference ref] loc ::
+      xmlApply ~loc
+        (xmlOperator ~loc "reference"
+           ~attr:["name", Libnames.string_of_reference ref] ::
          [Element ("impargs", [], []);
           Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
   | CPatCstr (ref, Some cpel1, cpel2) ->
-      xmlApply loc
-        (xmlOperator "reference"
-           ~attr:["name", Libnames.string_of_reference ref] loc ::
+      xmlApply ~loc
+        (xmlOperator ~loc "reference"
+           ~attr:["name", Libnames.string_of_reference ref] ::
          [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
           Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
   | CPatAtom optr ->
       let attrs = match optr with
         | None -> []
         | Some r -> ["name", Libnames.string_of_reference r] in
-      xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
+      xmlApply ~loc (xmlOperator ~loc "atom" ~attr:attrs :: [])
   | CPatOr cpel ->
-      xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
+      xmlApply ~loc (xmlOperator ~loc "or" :: List.map pp_cases_pattern_expr cpel)
   | CPatNotation (n, (subst_constr, subst_rec), cpel) ->
-      xmlApply loc
-        (xmlOperator "notation" loc ::
-          [xmlOperator n loc;
+      xmlApply ~loc
+        (xmlOperator ~loc "notation" ::
+          [xmlOperator ~loc n;
            Element ("subst", [],
              [Element ("subterms", [],
                 List.map pp_cases_pattern_expr subst_constr);
@@ -341,29 +341,29 @@ and pp_cases_pattern_expr (loc, cpe) =
                        List.map pp_cases_pattern_expr cpel))
                 subst_rec)]);
            Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
-  | CPatPrim tok   -> pp_token loc tok
+  | CPatPrim tok   -> pp_token ~loc tok
   | CPatRecord rcl ->
-      xmlApply loc
-        (xmlOperator "record" loc ::
+      xmlApply ~loc
+        (xmlOperator ~loc "record" ::
            List.map (fun (r, cpe) ->
              Element ("field",
                ["reference", Libnames.string_of_reference r],
                [pp_cases_pattern_expr cpe]))
            rcl)
   | CPatDelimiters (delim, cpe) ->
-      xmlApply loc
-        (xmlOperator "delimiter" ~attr:["name", delim] loc ::
+      xmlApply ~loc
+        (xmlOperator ~loc "delimiter" ~attr:["name", delim] ::
           [pp_cases_pattern_expr cpe])
   | CPatCast _ -> assert false
 and pp_case_expr (e, name, pat) =
   match name, pat with
   | None, None -> xmlScrutinee [pp_expr e]
   | Some (loc, name), None ->
-      let start, stop= unlock loc in
+      let start, stop= unlock ~loc in
       xmlScrutinee ~attr:["name", string_of_name name;
                           "begin", start; "end", stop] [pp_expr e]
   | Some (loc, name), Some p ->
-      let start, stop= unlock loc in
+      let start, stop= unlock ~loc in
       xmlScrutinee ~attr:["name", string_of_name name;
                           "begin", start; "end", stop]
         [Element ("in", [], [pp_cases_pattern_expr p]) ; pp_expr e]
@@ -378,12 +378,12 @@ and pp_branch_expr_list bel =
         let ppe = [pp_expr e] in
         xmlCase (ppcepl @ ppe))
      bel)
-and pp_token loc tok =
+and pp_token ?loc tok =
   let tokstr =
     match tok with
     | String s -> PCData s
     | Numeral n -> PCData (to_string n) in
-  xmlToken loc [tokstr]
+  xmlToken ?loc [tokstr]
 and pp_local_binder_list lbl =
   let l = (List.map pp_local_binder lbl) in
   Element ("recurse", (backstep_loc l), l)
@@ -393,142 +393,140 @@ and pp_const_expr_list cel =
 and pp_expr ?(attr=[]) (loc, e) =
   match e with
   | CRef (r, _) ->
-      xmlCst ~attr
-        (Libnames.string_of_reference r) (Libnames.loc_of_reference r)
+      xmlCst ~loc:(Libnames.loc_of_reference r) ~attr (Libnames.string_of_reference r)
   | CProdN (bl, e) ->
-      xmlApply loc
-        (xmlOperator "forall" loc :: [pp_bindlist bl] @ [pp_expr e])
+      xmlApply ~loc
+        (xmlOperator ~loc "forall" :: [pp_bindlist bl] @ [pp_expr e])
   | CApp ((_, hd), args) ->
-       xmlApply ~attr loc (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
+       xmlApply ~loc ~attr (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
   | CAppExpl ((_, r, _), args) ->
-       xmlApply ~attr loc
-         (xmlCst (Libnames.string_of_reference r)
-                 (Libnames.loc_of_reference r) :: List.map pp_expr args)
+       xmlApply ~loc ~attr
+         (xmlCst ~loc:(Libnames.loc_of_reference r) (Libnames.string_of_reference r)
+                 :: List.map pp_expr args)
   | CNotation (notation,  ([],[],[])) ->
-       xmlOperator notation loc
+       xmlOperator ~loc notation
   | CNotation (notation,  (args, cell, lbll)) ->
       let fmts = Notation.find_notation_extra_printing_rules notation in
-      let oper = xmlOperator notation loc ~pprules:fmts in
+      let oper = xmlOperator ~loc notation ~pprules:fmts in
       let cels = List.map pp_const_expr_list cell in
       let lbls = List.map pp_local_binder_list lbll in
       let args = List.map pp_expr args in
-      xmlApply loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls)))
+      xmlApply ~loc (oper :: (List.sort compare_begin_att (args @ cels @ lbls)))
   | CSort(s) ->
-      xmlOperator (string_of_glob_sort s) loc
+      xmlOperator ~loc (string_of_glob_sort s)
   | CDelimiters (scope, ce) ->
-      xmlApply loc (xmlOperator "delimiter" ~attr:["name", scope] loc ::
+      xmlApply ~loc (xmlOperator ~loc "delimiter" ~attr:["name", scope] ::
         [pp_expr ce])
-  | CPrim tok -> pp_token loc tok
+  | CPrim tok -> pp_token ~loc tok
   | CGeneralization (kind, _, e) ->
       let kind= match kind with
       | Explicit -> "explicit"
       | Implicit -> "implicit" in
-      xmlApply loc
-        (xmlOperator "generalization" ~attr:["kind", kind] loc :: [pp_expr e])
+      xmlApply ~loc
+        (xmlOperator ~loc ~attr:["kind", kind] "generalization" :: [pp_expr e])
   | CCast (e, tc) ->
       begin match tc with
       | CastConv t | CastVM t |CastNative t ->
-          xmlApply loc
-            (xmlOperator ":" loc ~attr:["kind", (string_of_cast_sort tc)] ::
+          xmlApply ~loc
+            (xmlOperator ~loc ":" ~attr:["kind", (string_of_cast_sort tc)] ::
              [pp_expr e; pp_expr t])
       | CastCoerce   ->
-          xmlApply loc
-            (xmlOperator ":" loc ~attr:["kind", "CastCoerce"] ::
+          xmlApply ~loc
+            (xmlOperator ~loc ":" ~attr:["kind", "CastCoerce"] ::
              [pp_expr e])
       end
   | CEvar (ek, cel) ->
       let ppcel = List.map (fun (id,e) -> xmlAssign id (pp_expr e)) cel in
-      xmlApply loc
-        (xmlOperator "evar" loc ~attr:["id", string_of_id ek] ::
+      xmlApply ~loc
+        (xmlOperator ~loc "evar" ~attr:["id", string_of_id ek] ::
           ppcel)
-  | CPatVar id -> xmlPatvar (string_of_id id) loc
-  | CHole (_, _, _) -> xmlCst ~attr  "_" loc
+  | CPatVar id -> xmlPatvar ~loc (string_of_id id)
+  | CHole (_, _, _) -> xmlCst ~loc ~attr  "_"
   | CIf (test, (_, ret), th, el) ->
       let return = match ret with
       | None -> []
       | Some r -> [xmlReturn [pp_expr r]] in
-      xmlApply loc
-        (xmlOperator "if" loc ::
+      xmlApply ~loc
+        (xmlOperator ~loc "if" ::
           return @ [pp_expr th] @ [pp_expr el])
   | CLetTuple (names, (_, ret), value, body) ->
       let return = match ret with
       | None -> []
       | Some r -> [xmlReturn [pp_expr r]] in
-      xmlApply loc
-        (xmlOperator "lettuple" loc ::
+      xmlApply ~loc
+        (xmlOperator ~loc "lettuple" ::
           return @
-          (List.map (fun (loc, var) -> xmlCst (string_of_name var) loc) names) @
+          (List.map (fun (loc, var) -> xmlCst ~loc (string_of_name var)) names) @
           [pp_expr value; pp_expr body])
   | CCases (sty, ret, cel, bel) ->
       let return = match ret with
       | None -> []
       | Some r -> [xmlReturn [pp_expr r]] in
-      xmlApply loc
-        (xmlOperator "match" loc  ~attr:["style", (string_of_case_style sty)] ::
+      xmlApply ~loc
+        (xmlOperator ~loc ~attr:["style", (string_of_case_style sty)] "match" ::
           (return @
            [Element ("scrutinees", [], List.map pp_case_expr cel)] @
            [pp_branch_expr_list bel]))
   | CRecord _ -> assert false
-
   | CLetIn ((varloc, var), value, typ, body) ->
       let (loc, value) = match typ with
         | Some t ->
           Loc.tag ~loc:(Loc.merge (constr_loc value) (constr_loc t)) (CCast (value, CastConv t))
         | None -> value in
-      xmlApply loc
-        (xmlOperator "let" loc ::
-         [xmlCst (string_of_name var) varloc; pp_expr (Loc.tag ~loc value); pp_expr body])
+      xmlApply ~loc
+        (xmlOperator ~loc "let" ::
+         [xmlCst ~loc:varloc (string_of_name var) ; pp_expr (Loc.tag ~loc value); pp_expr body])
   | CLambdaN (bl, e) ->
-      xmlApply loc
-        (xmlOperator "lambda" loc :: [pp_bindlist bl] @ [pp_expr e])
+      xmlApply ~loc
+        (xmlOperator ~loc "lambda" :: [pp_bindlist bl] @ [pp_expr e])
   | CCoFix (_, _) -> assert false
   | CFix (lid, fel) ->
-      xmlApply loc
-        (xmlOperator "fix" loc ::
+      xmlApply ~loc
+        (xmlOperator ~loc "fix" ::
            List.flatten (List.map
              (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d))
              fel))
 
-let pp_comment (c) =
+let pp_comment c =
   match c with
   | CommentConstr e -> [pp_expr e]
   | CommentString s -> [Element ("string", [], [PCData s])]
-  | CommentInt i -> [PCData (string_of_int i)]
+  | CommentInt i    -> [PCData (string_of_int i)]
 
-let rec tmpp v loc =
+let rec tmpp ?loc v =
   match v with
   (* Control *)
   | VernacLoad (verbose,f) ->
-      xmlWithLoc loc "load" ["verbose",string_of_bool verbose;"file",f] []
+      xmlWithLoc ?loc "load" ["verbose",string_of_bool verbose;"file",f] []
   | VernacTime (loc,e) ->
-      xmlApply loc (Element("time",[],[]) ::
-                    [tmpp e loc])
+      xmlApply ~loc (Element("time",[],[]) ::
+                    [tmpp ~loc e])
   | VernacRedirect (s, (loc,e)) ->
-      xmlApply loc (Element("redirect",["path", s],[]) ::
-                    [tmpp e loc])
+      xmlApply ~loc (Element("redirect",["path", s],[]) ::
+                    [tmpp ~loc e])
   | VernacTimeout (s,e) ->
-      xmlApply loc (Element("timeout",["val",string_of_int s],[]) ::
-                    [tmpp e loc])
-  | VernacFail e -> xmlApply loc (Element("fail",[],[]) :: [tmpp e loc])
+      xmlApply ?loc (Element("timeout",["val",string_of_int s],[]) ::
+                    [tmpp ?loc e])
+  | VernacFail e -> xmlApply ?loc (Element("fail",[],[]) :: [tmpp ?loc e])
 
   (* Syntax *)
   | VernacSyntaxExtension (_, ((_, name), sml)) ->
       let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
-      xmlReservedNotation attrs name loc
+      xmlReservedNotation ?loc attrs name
 
-  | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name []
-  | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name []
+  | VernacOpenCloseScope (_,(true,name)) -> xmlScope ?loc "open" name []
+  | VernacOpenCloseScope (_,(false,name)) -> xmlScope ?loc "close" name []
   | VernacDelimiters (name,Some tag) ->
-      xmlScope loc "delimit" name ~attr:["delimiter",tag] []
+      xmlScope ?loc "delimit" name ~attr:["delimiter",tag] []
   | VernacDelimiters (name,None) ->
-      xmlScope loc "undelimit" name ~attr:[] []
+      xmlScope ?loc "undelimit" name ~attr:[] []
   | VernacInfix (_,((_,name),sml),ce,sn) ->
       let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
       let sc_attr =
         match sn with
         | Some scope -> ["scope", scope]
         | None -> [] in
-      xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
+      xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce]
   | VernacNotation (_, ce, (lstr, sml), sn) ->
       let name = snd lstr in
       let attrs = List.flatten (List.map attribute_of_syntax_modifier sml) in
@@ -536,12 +534,12 @@ let rec tmpp v loc =
         match sn with
         | Some scope -> ["scope", scope]
         | None -> [] in
-      xmlNotation (sc_attr @ attrs) name loc [pp_expr ce]
-  | VernacBindScope _ as x -> xmlTODO loc x
-  | VernacNotationAddFormat _ as x -> xmlTODO loc x
+      xmlNotation ?loc (sc_attr @ attrs) name [pp_expr ce]
+  | VernacBindScope _ as x -> xmlTODO ?loc x
+  | VernacNotationAddFormat _ as x -> xmlTODO ?loc x
   | VernacUniverse _
   | VernacConstraint _
-  | VernacPolymorphic (_, _) as x -> xmlTODO loc x
+  | VernacPolymorphic (_, _) as x -> xmlTODO ?loc x
   (* Gallina *)
   | VernacDefinition (ldk, ((_,id),_), de) ->
       let l, dk =
@@ -557,26 +555,26 @@ let rec tmpp v loc =
         | DefineBody (_, None  , ce, Some _) -> ce in
       let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
       let str_id = Id.to_string id in
-      (xmlDef str_dk str_id loc [pp_expr e])
+      (xmlDef ?loc str_dk str_id [pp_expr e])
   | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
       let str_tk = Kindops.string_of_theorem_kind tk in
       let str_id = Id.to_string id in
-      (xmlThm str_tk str_id loc [pp_expr statement])
-  | VernacStartTheoremProof _ as x -> xmlTODO loc x
+      (xmlThm ?loc str_tk str_id [pp_expr statement])
+  | VernacStartTheoremProof _ as x -> xmlTODO ?loc x
   | VernacEndProof pe ->
       begin
         match pe with
-        | Admitted -> xmlQed loc
+        | Admitted -> xmlQed ?loc ?attr:None
         | Proved (_, Some ((_, id), Some tk)) ->
             let nam = Id.to_string id in
             let typ = Kindops.string_of_theorem_kind tk in
-            xmlQed ~attr:["name", nam; "type", typ] loc
+            xmlQed ?loc ~attr:["name", nam; "type", typ]
         | Proved (_, Some ((_, id), None)) ->
             let nam = Id.to_string id in
-            xmlQed ~attr:["name", nam] loc
-        | Proved _ -> xmlQed loc
+            xmlQed ?loc ~attr:["name", nam]
+        | Proved _ -> xmlQed ?loc ?attr:None
       end
-  | VernacExactProof _ as x -> xmlTODO loc x
+  | VernacExactProof _ as x -> xmlTODO ?loc x
   | VernacAssumption ((l, a), _, sbwcl) ->
       let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in
       let many =
@@ -585,7 +583,7 @@ let rec tmpp v loc =
         List.flatten (List.map pp_simple_binder binders) in
       let l = match l with Some x -> x | None -> Decl_kinds.Global in
       let kind = string_of_assumption_kind l a many in
-      xmlAssumption kind loc exprs
+      xmlAssumption ?loc kind exprs
   | VernacInductive (_, _, iednll) ->
       let kind =
         let (_, _, _, k, _),_ = List.hd iednll in
@@ -603,7 +601,7 @@ let rec tmpp v loc =
           (List.map
             (fun (ie, dnl) -> (pp_inductive_expr ie) @
                               (List.map pp_decl_notation dnl)) iednll) in
-      xmlInductive kind loc exprs
+      xmlInductive ?loc kind exprs
   | VernacFixpoint (_, fednll) ->
       let exprs =
         List.flatten (* should probably not be flattened *)
@@ -619,13 +617,13 @@ let rec tmpp v loc =
             (fun (cfe, dnl) -> (pp_cofixpoint_expr cfe) @
                               (List.map pp_decl_notation dnl)) cfednll) in
       xmlCoFixpoint exprs
-  | VernacScheme _ as x -> xmlTODO loc x
-  | VernacCombinedScheme _ as x -> xmlTODO loc x
+  | VernacScheme _ as x -> xmlTODO ?loc x
+  | VernacCombinedScheme _ as x -> xmlTODO ?loc x
 
   (* Gallina extensions *)
-  | VernacBeginSection (_, id) -> xmlBeginSection loc (Id.to_string id)
-  | VernacEndSegment (_, id) -> xmlEndSegment loc (Id.to_string id)
-  | VernacNameSectionHypSet _ as x -> xmlTODO loc x
+  | VernacBeginSection (_, id) -> xmlBeginSection ?loc (Id.to_string id)
+  | VernacEndSegment (_, id) -> xmlEndSegment ?loc (Id.to_string id)
+  | VernacNameSectionHypSet _ as x -> xmlTODO ?loc x
   | VernacRequire (from, import, l) ->
       let import = match import with
       | None -> []
@@ -636,137 +634,136 @@ let rec tmpp v loc =
       | None -> []
       | Some r -> ["from", Libnames.string_of_reference r]
       in
-      xmlRequire loc ~attr:(from @ import) (List.map (fun ref ->
+      xmlRequire ?loc ~attr:(from @ import) (List.map (fun ref ->
         xmlReference ref) l)
   | VernacImport (true,l) ->
-      xmlImport loc ~attr:["export","true"] (List.map (fun ref ->
+      xmlImport ?loc ~attr:["export","true"] (List.map (fun ref ->
         xmlReference ref) l)
   | VernacImport (false,l) ->
-      xmlImport loc (List.map (fun ref ->
-        xmlReference ref) l)
+      xmlImport ?loc (List.map (fun ref -> xmlReference ref) l)
   | VernacCanonical r ->
       let attr =
         match r with
         | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
         | AN (Ident (_, id)) -> ["id", Id.to_string id]
         | ByNotation (_, (s, _)) -> ["notation", s] in
-      xmlCanonicalStructure attr loc
-  | VernacCoercion _ as x -> xmlTODO loc x
-  | VernacIdentityCoercion _ as x -> xmlTODO loc x
+      xmlCanonicalStructure ?loc attr
+  | VernacCoercion _ as x -> xmlTODO ?loc x
+  | VernacIdentityCoercion _ as x -> xmlTODO ?loc x
 
   (* Type classes *)
-  | VernacInstance _ as x -> xmlTODO loc x
+  | VernacInstance _ as x -> xmlTODO ?loc x
 
-  | VernacContext _ as x -> xmlTODO loc x
+  | VernacContext _ as x -> xmlTODO ?loc x
 
-  | VernacDeclareInstances _ as x -> xmlTODO loc x
+  | VernacDeclareInstances _ as x -> xmlTODO ?loc x
 
-  | VernacDeclareClass _ as x -> xmlTODO loc x
+  | VernacDeclareClass _ as x -> xmlTODO ?loc x
 
   (* Modules and Module Types *)
-  | VernacDeclareModule _ as x -> xmlTODO loc x
-  | VernacDefineModule _ as x -> xmlTODO loc x
-  | VernacDeclareModuleType _ as x -> xmlTODO loc x
-  | VernacInclude _ as x -> xmlTODO loc x
+  | VernacDeclareModule _ as x -> xmlTODO ?loc x
+  | VernacDefineModule _ as x -> xmlTODO ?loc x
+  | VernacDeclareModuleType _ as x -> xmlTODO ?loc x
+  | VernacInclude _ as x -> xmlTODO ?loc x
 
   (* Solving *)
 
   | (VernacSolveExistential _) as x ->
-      xmlLtac loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+      xmlLtac ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
 
   (* Auxiliary file and library management *)
   | VernacAddLoadPath (recf,name,None) ->
-      xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name] []
+      xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name] []
   | VernacAddLoadPath (recf,name,Some dp) ->
-      xmlAddLoadPath loc ~attr:["rec",string_of_bool recf;"path",name]
+      xmlAddLoadPath ?loc ~attr:["rec",string_of_bool recf;"path",name]
         [PCData (Names.DirPath.to_string dp)]
-  | VernacRemoveLoadPath name -> xmlRemoveLoadPath loc ~attr:["path",name] []
+  | VernacRemoveLoadPath name -> xmlRemoveLoadPath ?loc ~attr:["path",name] []
   | VernacAddMLPath (recf,name) ->
-      xmlAddMLPath loc ~attr:["rec",string_of_bool recf;"path",name] []
-  | VernacDeclareMLModule sl -> xmlDeclareMLModule loc sl
-  | VernacChdir _ as x -> xmlTODO loc x
+      xmlAddMLPath ?loc ~attr:["rec",string_of_bool recf;"path",name] []
+  | VernacDeclareMLModule sl -> xmlDeclareMLModule ?loc sl
+  | VernacChdir _ as x -> xmlTODO ?loc x
 
   (* State management *)
-  | VernacWriteState _ as x -> xmlTODO loc x
-  | VernacRestoreState _ as x -> xmlTODO loc x
+  | VernacWriteState _ as x -> xmlTODO ?loc x
+  | VernacRestoreState _ as x -> xmlTODO ?loc x
 
   (* Resetting *)
-  | VernacResetName _ as x -> xmlTODO loc x
-  | VernacResetInitial as x -> xmlTODO loc x
-  | VernacBack _ as x -> xmlTODO loc x
+  | VernacResetName _ as x -> xmlTODO ?loc x
+  | VernacResetInitial as x -> xmlTODO ?loc x
+  | VernacBack _ as x -> xmlTODO ?loc x
   | VernacBackTo _ -> PCData "VernacBackTo"
 
   (* Commands *)
-  | VernacCreateHintDb _ as x -> xmlTODO loc x
-  | VernacRemoveHints _ as x -> xmlTODO loc x
-  | VernacHints _ as x -> xmlTODO loc x
+  | VernacCreateHintDb _ as x -> xmlTODO ?loc x
+  | VernacRemoveHints _ as x -> xmlTODO ?loc x
+  | VernacHints _ as x -> xmlTODO ?loc x
   | VernacSyntacticDefinition ((_, name), (idl, ce), _, _) ->
       let name = Id.to_string name in
       let attrs = List.map (fun id -> ("id", Id.to_string id)) idl in
-      xmlNotation attrs name loc [pp_expr ce]
-  | VernacDeclareImplicits _ as x -> xmlTODO loc x
-  | VernacArguments _ as x -> xmlTODO loc x
-  | VernacArgumentsScope _ as x -> xmlTODO loc x
-  | VernacReserve _ as x -> xmlTODO loc x
-  | VernacGeneralizable _ as x -> xmlTODO loc x
-  | VernacSetOpacity _ as x -> xmlTODO loc x
-  | VernacSetStrategy _ as x -> xmlTODO loc x
-  | VernacUnsetOption _ as x -> xmlTODO loc x
-  | VernacSetOption _ as x -> xmlTODO loc x
-  | VernacSetAppendOption _ as x -> xmlTODO loc x
-  | VernacAddOption _ as x -> xmlTODO loc x
-  | VernacRemoveOption _ as x -> xmlTODO loc x
-  | VernacMemOption _ as x -> xmlTODO loc x
-  | VernacPrintOption _ as x -> xmlTODO loc x
-  | VernacCheckMayEval (_,_,e) -> xmlCheck loc [pp_expr e]
-  | VernacGlobalCheck _ as x -> xmlTODO loc x
-  | VernacDeclareReduction _ as x -> xmlTODO loc x
-  | VernacPrint _ as x -> xmlTODO loc x
-  | VernacSearch _ as x -> xmlTODO loc x
-  | VernacLocate _ as x -> xmlTODO loc x
-  | VernacRegister _ as x -> xmlTODO loc x
+      xmlNotation ?loc attrs name [pp_expr ce]
+  | VernacDeclareImplicits _ as x -> xmlTODO ?loc x
+  | VernacArguments _ as x -> xmlTODO ?loc x
+  | VernacArgumentsScope _ as x -> xmlTODO ?loc x
+  | VernacReserve _ as x -> xmlTODO ?loc x
+  | VernacGeneralizable _ as x -> xmlTODO ?loc x
+  | VernacSetOpacity _ as x -> xmlTODO ?loc x
+  | VernacSetStrategy _ as x -> xmlTODO ?loc x
+  | VernacUnsetOption _ as x -> xmlTODO ?loc x
+  | VernacSetOption _ as x -> xmlTODO ?loc x
+  | VernacSetAppendOption _ as x -> xmlTODO ?loc x
+  | VernacAddOption _ as x -> xmlTODO ?loc x
+  | VernacRemoveOption _ as x -> xmlTODO ?loc x
+  | VernacMemOption _ as x -> xmlTODO ?loc x
+  | VernacPrintOption _ as x -> xmlTODO ?loc x
+  | VernacCheckMayEval (_,_,e) -> xmlCheck ?loc [pp_expr e]
+  | VernacGlobalCheck _ as x -> xmlTODO ?loc x
+  | VernacDeclareReduction _ as x -> xmlTODO ?loc x
+  | VernacPrint _ as x -> xmlTODO ?loc x
+  | VernacSearch _ as x -> xmlTODO ?loc x
+  | VernacLocate _ as x -> xmlTODO ?loc x
+  | VernacRegister _ as x -> xmlTODO ?loc x
   | VernacComments (cl) ->
-      xmlComment loc (List.flatten (List.map pp_comment cl))
+      xmlComment ?loc (List.flatten (List.map pp_comment cl))
 
   (* Stm backdoor *)
-  | VernacStm _ as x -> xmlTODO loc x
+  | VernacStm _ as x -> xmlTODO ?loc x
 
   (* Proof management *)
-  | VernacGoal _ as x -> xmlTODO loc x
-  | VernacAbort _ as x -> xmlTODO loc x
+  | VernacGoal _ as x -> xmlTODO ?loc x
+  | VernacAbort _ as x -> xmlTODO ?loc x
   | VernacAbortAll -> PCData "VernacAbortAll"
-  | VernacRestart as x -> xmlTODO loc x
-  | VernacUndo _ as x -> xmlTODO loc x
-  | VernacUndoTo _ as x -> xmlTODO loc x
-  | VernacBacktrack _ as x -> xmlTODO loc x
-  | VernacFocus _ as x -> xmlTODO loc x
-  | VernacUnfocus as x -> xmlTODO loc x
-  | VernacUnfocused as x -> xmlTODO loc x
-  | VernacBullet _ as x -> xmlTODO loc x
-  | VernacSubproof _ as x -> xmlTODO loc x
-  | VernacEndSubproof as x -> xmlTODO loc x
-  | VernacShow _ as x -> xmlTODO loc x
-  | VernacCheckGuard as x -> xmlTODO loc x
+  | VernacRestart as x -> xmlTODO ?loc x
+  | VernacUndo _ as x -> xmlTODO ?loc x
+  | VernacUndoTo _ as x -> xmlTODO ?loc x
+  | VernacBacktrack _ as x -> xmlTODO ?loc x
+  | VernacFocus _ as x -> xmlTODO ?loc x
+  | VernacUnfocus as x -> xmlTODO ?loc x
+  | VernacUnfocused as x -> xmlTODO ?loc x
+  | VernacBullet _ as x -> xmlTODO ?loc x
+  | VernacSubproof _ as x -> xmlTODO ?loc x
+  | VernacEndSubproof as x -> xmlTODO ?loc x
+  | VernacShow _ as x -> xmlTODO ?loc x
+  | VernacCheckGuard as x -> xmlTODO ?loc x
   | VernacProof (tac,using) ->
       let tac = None (** FIXME *) in
       let using = Option.map (xmlSectionSubsetDescr "using") using in
-      xmlProof loc (Option.List.(cons tac (cons using [])))
-  | VernacProofMode name -> xmlProofMode loc name
+      xmlProof ?loc (Option.List.(cons tac (cons using [])))
+  | VernacProofMode name -> xmlProofMode ?loc name
 
   (* Toplevel control *)
-  | VernacToplevelControl _ as x -> xmlTODO loc x
+  | VernacToplevelControl _ as x -> xmlTODO ?loc x
 
   (* For extension *)
   | VernacExtend _ as x ->
-      xmlExtend loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
+      xmlExtend ?loc [PCData (Pp.string_of_ppcmds (Ppvernac.pr_vernac x))]
 
   (* Flags *)
-  | VernacProgram e -> xmlApply loc (Element("program",[],[]) :: [tmpp e loc])
+  | VernacProgram e -> xmlApply ?loc (Element("program",[],[]) :: [tmpp ?loc e])
   | VernacLocal (b,e) ->
-      xmlApply loc (Element("local",["flag",string_of_bool b],[]) ::
-                    [tmpp e loc])
+      xmlApply ?loc (Element("local",["flag",string_of_bool b],[]) ::
+                    [tmpp ?loc e])
 
-let tmpp v loc =
-  match tmpp v loc with
+let tmpp ?loc v =
+  match tmpp ?loc v with
   | Element("ltac",_,_) as x -> x
-  | xml -> xmlGallina loc [xml]
+  | xml -> xmlGallina ?loc [xml]
diff --git a/ide/texmacspp.mli b/ide/texmacspp.mli
index 858847fb6..c1086a633 100644
--- a/ide/texmacspp.mli
+++ b/ide/texmacspp.mli
@@ -9,4 +9,4 @@
 open Xml_datatype
 open Vernacexpr
 
-val tmpp : vernac_expr -> Loc.t -> xml
+val tmpp : ?loc:Loc.t -> vernac_expr -> xml
diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml
index bf52b0b52..53eb1a95f 100644
--- a/ide/xmlprotocol.ml
+++ b/ide/xmlprotocol.ml
@@ -863,7 +863,7 @@ let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
   | "workerstatus", [ns] ->
        let n, s = to_pair to_string to_string ns in
        WorkerStatus(n,s)
-  | "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x)
+  | "custom", [loc;name;x]-> Custom (to_option to_loc loc, to_string name, x)
   | "filedependency", [from; dep] ->
       FileDependency (to_option to_string from, to_string dep)
   | "fileloaded", [dirpath; filename] ->
@@ -896,7 +896,7 @@ let of_feedback_content = function
       constructor "feedback_content" "workerstatus"
         [of_pair of_string of_string (n,s)]
   | Custom (loc, name, x) ->
-      constructor "feedback_content" "custom" [of_loc loc; of_string name; x]
+      constructor "feedback_content" "custom" [of_option of_loc loc; of_string name; x]
   | FileDependency (from, depends_on) ->
       constructor "feedback_content" "filedependency" [
         of_option of_string from;