From 846b74275511bd89c2f3abe19245133050d2199c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 12 Jan 2017 20:11:01 +0100
Subject: [constrexpr] Make patterns use Loc.located for location information

This is first of a series of patches, converting `constrexpr` pattern
data type from ad-hoc location handling to `Loc.located`.

Along Coq, we can find two different coding styles for handling
objects with location information: one style uses `'a Loc.located`,
whereas other data structures directly embed `Loc.t` in their
constructors.

Handling all located objects uniformly would be very convenient, and
would allow optimizing certain cases, in particular making located
smarter when there is no location information, as it is the case for
all terms coming from the kernel.

`git grep 'Loc.t \*'` gives an overview of the remaining work to do.

We've also added an experimental API for `located` to the `Loc`
module, `Loc.tag` should be used to add locations objects, making it
explicit in the code when a "located" object is created.
---
 ide/texmacspp.ml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index e20704b7fb..19be13be78 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -300,32 +300,32 @@ and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
   end
 and pp_lident (loc, id) = xmlCst (Id.to_string id) loc
 and pp_simple_binder (idl, ce) = List.map pp_lident idl @ [pp_expr ce]
-and pp_cases_pattern_expr cpe =
+and pp_cases_pattern_expr (loc, cpe) =
   match cpe with
-  | CPatAlias (loc, cpe, id) ->
+  | CPatAlias (cpe, id) ->
       xmlApply loc
         (xmlOperator "alias" ~attr:["name", string_of_id id] loc ::
           [pp_cases_pattern_expr cpe])
-  | CPatCstr (loc, ref, None, cpel2) ->
+  | CPatCstr (ref, None, cpel2) ->
       xmlApply loc
         (xmlOperator "reference"
            ~attr:["name", Libnames.string_of_reference ref] loc ::
          [Element ("impargs", [], []);
           Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
-  | CPatCstr (loc, ref, Some cpel1, cpel2) ->
+  | CPatCstr (ref, Some cpel1, cpel2) ->
       xmlApply loc
         (xmlOperator "reference"
            ~attr:["name", Libnames.string_of_reference ref] loc ::
          [Element ("impargs", [], (List.map pp_cases_pattern_expr cpel1));
           Element ("args", [], (List.map pp_cases_pattern_expr cpel2))])
-  | CPatAtom (loc, optr) ->
+  | CPatAtom optr ->
       let attrs = match optr with
         | None -> []
         | Some r -> ["name", Libnames.string_of_reference r] in
       xmlApply loc (xmlOperator "atom" ~attr:attrs loc :: [])
-  | CPatOr (loc, cpel) ->
+  | CPatOr cpel ->
       xmlApply loc (xmlOperator "or" loc :: List.map pp_cases_pattern_expr cpel)
-  | CPatNotation (loc, n, (subst_constr, subst_rec), cpel) ->
+  | CPatNotation (n, (subst_constr, subst_rec), cpel) ->
       xmlApply loc
         (xmlOperator "notation" loc ::
           [xmlOperator n loc;
@@ -339,8 +339,8 @@ and pp_cases_pattern_expr cpe =
                        List.map pp_cases_pattern_expr cpel))
                 subst_rec)]);
            Element ("args", [], (List.map pp_cases_pattern_expr cpel))])
-  | CPatPrim (loc, tok) -> pp_token loc tok
-  | CPatRecord (loc, rcl) ->
+  | CPatPrim tok   -> pp_token loc tok
+  | CPatRecord rcl ->
       xmlApply loc
         (xmlOperator "record" loc ::
            List.map (fun (r, cpe) ->
@@ -348,7 +348,7 @@ and pp_cases_pattern_expr cpe =
                ["reference", Libnames.string_of_reference r],
                [pp_cases_pattern_expr cpe]))
            rcl)
-  | CPatDelimiters (loc, delim, cpe) ->
+  | CPatDelimiters (delim, cpe) ->
       xmlApply loc
         (xmlOperator "delimiter" ~attr:["name", delim] loc ::
           [pp_cases_pattern_expr cpe])
@@ -370,7 +370,7 @@ and pp_case_expr (e, name, pat) =
 and pp_branch_expr_list bel =
   xmlWith
     (List.map
-      (fun (_, cpel, e) ->
+      (fun (_, (cpel, e)) ->
         let ppcepl =
           List.map pp_cases_pattern_expr (List.flatten (List.map snd cpel)) in
         let ppe = [pp_expr e] in
-- 
cgit v1.2.3


From 6d9e008ffd81bbe927e3442fb0c37269ed25b21f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 14 Jan 2017 01:27:40 +0100
Subject: [location] Use Loc.located for constr_expr.

This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.

Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.
---
 ide/texmacspp.ml | 58 +++++++++++++++++++++++++++++++-------------------------
 1 file changed, 32 insertions(+), 26 deletions(-)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 19be13be78..77dca0d06f 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -219,7 +219,7 @@ let rec pp_bindlist bl =
                 (fun (loc, name) ->
                   xmlCst (string_of_name name) loc) loc_names) in
             match e with
-              | CHole _ -> names
+              | _, CHole _ -> names
               | _ -> names @ [pp_expr e])
           bl) in
   match tlist with
@@ -231,7 +231,9 @@ and pp_local_binder lb = (* don't know what it is for now *)
   match lb with
   | CLocalDef ((loc, nam), ce, ty) ->
       let attrs = ["name", string_of_name nam] in
-      let value = match ty with Some t -> CCast (Loc.merge (constr_loc ce) (constr_loc t),ce, CastConv t) | None -> ce in
+      let value = match ty with
+          Some t -> Loc.tag ~loc:(Loc.merge (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t)
+        | None -> ce in
       pp_expr ~attr:attrs value
   | CLocalAssum (namll, _, ce) ->
       let ppl =
@@ -388,42 +390,42 @@ and pp_local_binder_list lbl =
 and pp_const_expr_list cel =
   let l = List.map pp_expr cel in
   Element ("recurse", (backstep_loc l), l)
-and pp_expr ?(attr=[]) e =
+and pp_expr ?(attr=[]) (loc, e) =
   match e with
   | CRef (r, _) ->
       xmlCst ~attr
         (Libnames.string_of_reference r) (Libnames.loc_of_reference r)
-  | CProdN (loc, bl, e) ->
+  | CProdN (bl, e) ->
       xmlApply loc
         (xmlOperator "forall" loc :: [pp_bindlist bl] @ [pp_expr e])
-  | CApp (loc, (_, hd), args) ->
+  | CApp ((_, hd), args) ->
        xmlApply ~attr loc (pp_expr hd :: List.map (fun (e,_) -> pp_expr e) args)
-  | CAppExpl (loc, (_, r, _), args) ->
+  | CAppExpl ((_, r, _), args) ->
        xmlApply ~attr loc
          (xmlCst (Libnames.string_of_reference r)
                  (Libnames.loc_of_reference r) :: List.map pp_expr args)
-  | CNotation (loc, notation,  ([],[],[])) ->
+  | CNotation (notation,  ([],[],[])) ->
        xmlOperator notation loc
-  | CNotation (loc, notation,  (args, cell, lbll)) ->
+  | CNotation (notation,  (args, cell, lbll)) ->
       let fmts = Notation.find_notation_extra_printing_rules notation in
       let oper = xmlOperator notation loc ~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)))
-  | CSort(loc, s) ->
+  | CSort(s) ->
       xmlOperator (string_of_glob_sort s) loc
-  | CDelimiters (loc, scope, ce) ->
+  | CDelimiters (scope, ce) ->
       xmlApply loc (xmlOperator "delimiter" ~attr:["name", scope] loc ::
         [pp_expr ce])
-  | CPrim (loc, tok) -> pp_token loc tok
-  | CGeneralization (loc, kind, _, e) ->
+  | 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])
-  | CCast (loc, e, tc) ->
+  | CCast (e, tc) ->
       begin match tc with
       | CastConv t | CastVM t |CastNative t ->
           xmlApply loc
@@ -434,21 +436,21 @@ and pp_expr ?(attr=[]) e =
             (xmlOperator ":" loc ~attr:["kind", "CastCoerce"] ::
              [pp_expr e])
       end
-  | CEvar (loc, ek, cel) ->
+  | 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] ::
           ppcel)
-  | CPatVar (loc, id) -> xmlPatvar (string_of_id id) loc
-  | CHole (loc, _, _, _) -> xmlCst ~attr  "_" loc
-  | CIf (loc, test, (_, ret), th, el) ->
+  | CPatVar id -> xmlPatvar (string_of_id id) loc
+  | CHole (_, _, _) -> xmlCst ~attr  "_" loc
+  | CIf (test, (_, ret), th, el) ->
       let return = match ret with
       | None -> []
       | Some r -> [xmlReturn [pp_expr r]] in
       xmlApply loc
         (xmlOperator "if" loc ::
           return @ [pp_expr th] @ [pp_expr el])
-  | CLetTuple (loc, names, (_, ret), value, body) ->
+  | CLetTuple (names, (_, ret), value, body) ->
       let return = match ret with
       | None -> []
       | Some r -> [xmlReturn [pp_expr r]] in
@@ -457,7 +459,7 @@ and pp_expr ?(attr=[]) e =
           return @
           (List.map (fun (loc, var) -> xmlCst (string_of_name var) loc) names) @
           [pp_expr value; pp_expr body])
-  | CCases (loc, sty, ret, cel, bel) ->
+  | CCases (sty, ret, cel, bel) ->
       let return = match ret with
       | None -> []
       | Some r -> [xmlReturn [pp_expr r]] in
@@ -466,17 +468,21 @@ and pp_expr ?(attr=[]) e =
           (return @
            [Element ("scrutinees", [], List.map pp_case_expr cel)] @
            [pp_branch_expr_list bel]))
-  | CRecord (_, _) -> assert false
-  | CLetIn (loc, (varloc, var), value, typ, body) ->
-      let value = match typ with Some t -> CCast (Loc.merge (constr_loc value) (constr_loc t),value, CastConv t) | None -> value in
+  | 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 value; pp_expr body])
-  | CLambdaN (loc, bl, e) ->
+         [xmlCst (string_of_name var) varloc; pp_expr (Loc.tag ~loc value); pp_expr body])
+  | CLambdaN (bl, e) ->
       xmlApply loc
         (xmlOperator "lambda" loc :: [pp_bindlist bl] @ [pp_expr e])
-  | CCoFix (_, _, _) -> assert false
-  | CFix (loc, lid, fel) ->
+  | CCoFix (_, _) -> assert false
+  | CFix (lid, fel) ->
       xmlApply loc
         (xmlOperator "fix" loc ::
            List.flatten (List.map
-- 
cgit v1.2.3


From bf13037e9ca39da28fb648e5488ce56ef8a1f1e2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 15:06:26 +0100
Subject: [location] Use located in misctypes.

---
 ide/texmacspp.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 77dca0d06f..f86b260df5 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -649,7 +649,7 @@ let rec tmpp v loc =
         match r with
         | AN (Qualid (_, q)) -> ["qualid", string_of_qualid q]
         | AN (Ident (_, id)) -> ["id", Id.to_string id]
-        | ByNotation (_, s, _) -> ["notation", s] in
+        | ByNotation (_, (s, _)) -> ["notation", s] in
       xmlCanonicalStructure attr loc
   | VernacCoercion _ as x -> xmlTODO loc x
   | VernacIdentityCoercion _ as x -> xmlTODO loc x
-- 
cgit v1.2.3


From 30d3515546cf244837c6340b6b87c5f51e68cbf4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 17 Jan 2017 23:40:35 +0100
Subject: [location] Remove Loc.ghost.

Now it is a private field, locations are optional.
---
 ide/coqOps.ml      |  22 +--
 ide/ide_slave.ml   |   4 +-
 ide/texmacspp.ml   | 449 ++++++++++++++++++++++++++---------------------------
 ide/texmacspp.mli  |   2 +-
 ide/xmlprotocol.ml |   4 +-
 5 files changed, 240 insertions(+), 241 deletions(-)

(limited to 'ide')

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 222b9eed9f..7825fb45e1 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 bf86db08ff..7f30a4acc0 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 f86b260df5..0a07a830b3 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 858847fb6a..c1086a6339 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 bf52b0b52b..53eb1a95ff 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;
-- 
cgit v1.2.3


From e8a6467545c2814c9418889201e8be19c0cef201 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 18 Jan 2017 15:46:23 +0100
Subject: [location] Make location optional in Loc.located

This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.

We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.

The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
---
 ide/coqOps.ml    |  23 ++++-----
 ide/ide_slave.ml |  10 ++--
 ide/texmacspp.ml | 140 +++++++++++++++++++++++++++----------------------------
 3 files changed, 84 insertions(+), 89 deletions(-)

(limited to 'ide')

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 7825fb45e1..50d0dc4913 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -14,7 +14,7 @@ open Feedback
 
 let b2c = byte_offset_to_char_offset
 
-type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of Loc.t * string | `WARNING of Loc.t * string ]
+type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of string Loc.located | `WARNING of string Loc.located ]
 type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR | `WARNING ]
 let mem_flag_of_flag : flag -> mem_flag = function
   | `ERROR _ -> `ERROR
@@ -467,19 +467,15 @@ object(self)
       | Message(Error, loc, msg), Some (id,sentence) ->
           log_pp ?id Pp.(str "ErrorMsg" ++ msg);
           remove_flag sentence `PROCESSING;
-          let rmsg = Pp.string_of_ppcmds msg     in
-          Option.iter (fun loc ->
-              add_flag sentence (`ERROR (loc, rmsg));
-            ) loc;
+          let rmsg = Pp.string_of_ppcmds msg in
+          add_flag sentence (`ERROR (loc, rmsg));
           self#mark_as_needed sentence;
           self#attach_tooltip ?loc sentence rmsg;
           self#position_tag_at_sentence ?loc Tags.Script.error sentence
       | Message(Warning, loc, msg), Some (id,sentence) ->
           log_pp ?id Pp.(str "WarningMsg" ++ msg);
           let rmsg = Pp.string_of_ppcmds msg     in
-          Option.iter (fun loc ->
-              add_flag sentence (`WARNING (loc, rmsg));
-            ) loc;
+          add_flag sentence (`WARNING (loc, rmsg));
           self#attach_tooltip ?loc sentence rmsg;
           self#position_tag_at_sentence ?loc Tags.Script.warning sentence;
           messages#push Warning msg
@@ -683,14 +679,13 @@ object(self)
     let extract_error s =
       match List.find (function `ERROR _ -> true | _ -> false) s.flags with
       | `ERROR (loc, msg) ->
-         let iter =
-           if Loc.is_ghost loc then
-             buffer#get_iter_at_mark s.start
-           else
+         let iter = begin match loc with
+           | None      -> buffer#get_iter_at_mark s.start
+           | Some loc ->
              let (iter, _, phrase) = self#get_sentence s in
              let (start, _) = Loc.unloc loc in
-             iter#forward_chars (b2c phrase start) in
-         iter#line + 1, msg
+             iter#forward_chars (b2c phrase start)
+         end in iter#line + 1, msg
       | _ -> assert false in
     List.rev
       (Doc.fold_all document [] (fun acc _ _ s ->
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 7f30a4acc0..bbc3e4bcb8 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -64,8 +64,8 @@ let is_known_option cmd = match cmd with
 (** Check whether a command is forbidden in the IDE *)
 
 let ide_cmd_checks ~id (loc,ast) =
-  let user_error s = CErrors.user_err ~loc ~hdr:"CoqIde" (str s) in
-  let warn msg = Feedback.(feedback ~id (Message (Warning, Some loc, strbrk msg))) in
+  let user_error s = CErrors.user_err ?loc ~hdr:"CoqIde" (str s) in
+  let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
   if is_debug ast then
     user_error "Debug mode not available in the IDE";
   if is_known_option ast then
@@ -342,8 +342,8 @@ let about () = {
 let handle_exn (e, info) =
   let dummy = Stateid.dummy in
   let loc_of e = match Loc.get_loc e with
-    | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
-    | _ -> None in
+    | Some loc -> Some (Loc.unloc loc)
+    | _        -> None in
   let mk_msg () = CErrors.print ~info e in
   match e with
   | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!"
@@ -391,7 +391,7 @@ let quit = ref false
 let print_ast id =
   match Stm.get_ast id with
   | Some (loc, expr) -> begin
-      try  Texmacspp.tmpp ~loc expr
+      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 0a07a830b3..071861e271 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -108,7 +108,7 @@ let xmlPatvar ?loc id = xmlWithLoc ?loc "patvar" ["id", id] []
 
 let xmlReference ref =
   let name = Libnames.string_of_reference ref in
-  let i, j = Loc.unloc (Libnames.loc_of_reference ref) in
+  let i, j = Option.cata Loc.unloc (0,0) (Libnames.loc_of_reference ref) in
   let b, e = string_of_int i, string_of_int j in
   Element("reference",["name", name; "begin", b; "end", e] ,[])
 
@@ -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 ~loc (string_of_name name)) loc_names) in
+                  xmlCst ?loc (string_of_name name)) loc_names) in
             match e with
               | _, CHole _ -> names
               | _ -> names @ [pp_expr e])
@@ -232,12 +232,12 @@ and pp_local_binder lb = (* don't know what it is for now *)
   | CLocalDef ((loc, nam), ce, ty) ->
       let attrs = ["name", string_of_name nam] in
       let value = match ty with
-          Some t -> Loc.tag ~loc:(Loc.merge (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t)
+          Some t -> Loc.tag ?loc:(Loc.merge_opt (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t)
         | None -> ce in
       pp_expr ~attr:attrs value
   | CLocalAssum (namll, _, ce) ->
       let ppl =
-        List.map (fun (loc, nam) -> (xmlCst ~loc (string_of_name nam))) namll in
+        List.map (fun (loc, nam) -> (xmlCst ?loc (string_of_name nam))) namll in
       xmlTyped (ppl @ [pp_expr ce])
   | CLocalPattern _ ->
       assert false
@@ -247,7 +247,7 @@ and pp_local_decl_expr lde = (* don't know what it is for now *)
   | DefExpr (_, ce, _) -> pp_expr ce
 and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) =
   (* inductive_expr *)
-  let b,e = Loc.unloc l in
+  let b,e = Option.cata Loc.unloc (0,0) l in
   let location = ["begin", string_of_int b; "end", string_of_int e] in
   [Element ("lident", ["name", Id.to_string id] @ location, [])] @ (* inductive name *)
   begin match cl_or_rdexpr with
@@ -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,23 +300,23 @@ 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 ~loc (Id.to_string id)
+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 ~loc ~attr:["name", string_of_id id] "alias" ::
+      xmlApply ?loc
+        (xmlOperator ?loc ~attr:["name", string_of_id id] "alias" ::
           [pp_cases_pattern_expr cpe])
   | CPatCstr (ref, None, cpel2) ->
-      xmlApply ~loc
-        (xmlOperator ~loc "reference"
+      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 ~loc "reference"
+      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))])
@@ -324,13 +324,13 @@ and pp_cases_pattern_expr (loc, cpe) =
       let attrs = match optr with
         | None -> []
         | Some r -> ["name", Libnames.string_of_reference r] in
-      xmlApply ~loc (xmlOperator ~loc "atom" ~attr:attrs :: [])
+      xmlApply ?loc (xmlOperator ?loc "atom" ~attr:attrs :: [])
   | CPatOr cpel ->
-      xmlApply ~loc (xmlOperator ~loc "or" :: 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 ~loc "notation" ::
-          [xmlOperator ~loc n;
+      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 ~loc "record" ::
+      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 ~loc "delimiter" ~attr:["name", delim] ::
+      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]
@@ -393,77 +393,77 @@ and pp_const_expr_list cel =
 and pp_expr ?(attr=[]) (loc, e) =
   match e with
   | CRef (r, _) ->
-      xmlCst ~loc:(Libnames.loc_of_reference r) ~attr (Libnames.string_of_reference r)
+      xmlCst ?loc:(Libnames.loc_of_reference r) ~attr (Libnames.string_of_reference r)
   | CProdN (bl, e) ->
-      xmlApply ~loc
-        (xmlOperator ~loc "forall" :: [pp_bindlist bl] @ [pp_expr e])
+      xmlApply ?loc
+        (xmlOperator ?loc "forall" :: [pp_bindlist bl] @ [pp_expr e])
   | CApp ((_, hd), args) ->
-       xmlApply ~loc ~attr (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 ~loc ~attr
-         (xmlCst ~loc:(Libnames.loc_of_reference r) (Libnames.string_of_reference r)
+       xmlApply ?loc ~attr
+         (xmlCst ?loc:(Libnames.loc_of_reference r) (Libnames.string_of_reference r)
                  :: List.map pp_expr args)
   | CNotation (notation,  ([],[],[])) ->
-       xmlOperator ~loc notation
+       xmlOperator ?loc notation
   | CNotation (notation,  (args, cell, lbll)) ->
       let fmts = Notation.find_notation_extra_printing_rules notation in
-      let oper = xmlOperator ~loc notation ~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 ~loc (string_of_glob_sort s)
+      xmlOperator ?loc (string_of_glob_sort s)
   | CDelimiters (scope, ce) ->
-      xmlApply ~loc (xmlOperator ~loc "delimiter" ~attr:["name", scope] ::
+      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 ~loc ~attr:["kind", kind] "generalization" :: [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 ~loc "evar" ~attr:["id", string_of_id ek] ::
+      xmlApply ?loc
+        (xmlOperator ?loc "evar" ~attr:["id", string_of_id ek] ::
           ppcel)
-  | CPatVar id -> xmlPatvar ~loc (string_of_id id)
-  | CHole (_, _, _) -> xmlCst ~loc ~attr  "_"
+  | 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 ~loc "if" ::
+      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 ~loc "lettuple" ::
+      xmlApply ?loc
+        (xmlOperator ?loc "lettuple" ::
           return @
-          (List.map (fun (loc, var) -> xmlCst ~loc (string_of_name var)) 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 ~loc ~attr:["style", (string_of_case_style sty)] "match" ::
+      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]))
@@ -471,18 +471,18 @@ and pp_expr ?(attr=[]) (loc, e) =
   | 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))
+          Loc.tag ?loc:(Loc.merge_opt (constr_loc value) (constr_loc t)) (CCast (value, CastConv t))
         | None -> value in
-      xmlApply ~loc
-        (xmlOperator ~loc "let" ::
-         [xmlCst ~loc:varloc (string_of_name var) ; 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 ~loc "lambda" :: [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 ~loc "fix" ::
+      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))
@@ -499,11 +499,11 @@ let rec tmpp ?loc v =
   | VernacLoad (verbose,f) ->
       xmlWithLoc ?loc "load" ["verbose",string_of_bool verbose;"file",f] []
   | VernacTime (loc,e) ->
-      xmlApply ~loc (Element("time",[],[]) ::
-                    [tmpp ~loc e])
+      xmlApply ?loc (Element("time",[],[]) ::
+                    [tmpp ?loc e])
   | VernacRedirect (s, (loc,e)) ->
-      xmlApply ~loc (Element("redirect",["path", s],[]) ::
-                    [tmpp ~loc e])
+      xmlApply ?loc (Element("redirect",["path", s],[]) ::
+                    [tmpp ?loc e])
   | VernacTimeout (s,e) ->
       xmlApply ?loc (Element("timeout",["val",string_of_int s],[]) ::
                     [tmpp ?loc e])
@@ -586,7 +586,7 @@ let rec tmpp ?loc v =
       xmlAssumption ?loc kind exprs
   | VernacInductive (_, _, iednll) ->
       let kind =
-        let (_, _, _, k, _),_ = List.hd iednll in
+        let (_, _, _, k, _), _ = List.hd iednll in
 	  begin
             match k with
             | Record -> "Record"
-- 
cgit v1.2.3


From 054d2736c1c1b55cb7708ff0444af521cd0fe2ba Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 8 Apr 2017 23:19:35 +0200
Subject: [location] [ast] Switch Constrexpr AST to an extensible node type.

Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.

This provides significantly clearer code for the AST, and is robust
wrt attributes.
---
 ide/texmacspp.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'ide')

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 071861e271..ddb62313ff 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -218,8 +218,8 @@ let rec pp_bindlist bl =
               (List.map
                 (fun (loc, name) ->
                   xmlCst ?loc (string_of_name name)) loc_names) in
-            match e with
-              | _, CHole _ -> names
+            match e.CAst.v with
+              | CHole _ -> names
               | _ -> names @ [pp_expr e])
           bl) in
   match tlist with
@@ -232,7 +232,7 @@ and pp_local_binder lb = (* don't know what it is for now *)
   | CLocalDef ((loc, nam), ce, ty) ->
       let attrs = ["name", string_of_name nam] in
       let value = match ty with
-          Some t -> Loc.tag ?loc:(Loc.merge_opt (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t)
+          Some t -> CAst.make ?loc:(Loc.merge_opt (constr_loc ce) (constr_loc t)) @@ CCast (ce, CastConv t)
         | None -> ce in
       pp_expr ~attr:attrs value
   | CLocalAssum (namll, _, ce) ->
@@ -302,7 +302,7 @@ and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *)
   end
 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) =
+and pp_cases_pattern_expr {loc ; CAst.v = cpe} =
   match cpe with
   | CPatAlias (cpe, id) ->
       xmlApply ?loc
@@ -390,7 +390,7 @@ and pp_local_binder_list lbl =
 and pp_const_expr_list cel =
   let l = List.map pp_expr cel in
   Element ("recurse", (backstep_loc l), l)
-and pp_expr ?(attr=[]) (loc, e) =
+and pp_expr ?(attr=[]) { loc; CAst.v = e } =
   match e with
   | CRef (r, _) ->
       xmlCst ?loc:(Libnames.loc_of_reference r) ~attr (Libnames.string_of_reference r)
@@ -469,13 +469,13 @@ and pp_expr ?(attr=[]) (loc, e) =
            [pp_branch_expr_list bel]))
   | CRecord _ -> assert false
   | CLetIn ((varloc, var), value, typ, body) ->
-      let (loc, value) = match typ with
+      let value = match typ with
         | Some t ->
-          Loc.tag ?loc:(Loc.merge_opt (constr_loc value) (constr_loc t)) (CCast (value, CastConv t))
+          CAst.make ?loc:(Loc.merge_opt (constr_loc value) (constr_loc t)) (CCast (value, CastConv t))
         | None -> value in
       xmlApply ?loc
         (xmlOperator ?loc "let" ::
-         [xmlCst ?loc:varloc (string_of_name var) ; pp_expr (Loc.tag ?loc value); pp_expr body])
+         [xmlCst ?loc:varloc (string_of_name var) ; pp_expr value; pp_expr body])
   | CLambdaN (bl, e) ->
       xmlApply ?loc
         (xmlOperator ?loc "lambda" :: [pp_bindlist bl] @ [pp_expr e])
-- 
cgit v1.2.3