diff options
| author | Emilio Jesus Gallego Arias | 2017-01-18 15:46:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-25 00:28:53 +0200 |
| commit | e8a6467545c2814c9418889201e8be19c0cef201 (patch) | |
| tree | 7f513d854b76b02f52f98ee0e87052c376175a0f /printing/ppvernac.ml | |
| parent | 30d3515546cf244837c6340b6b87c5f51e68cbf4 (diff) | |
[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.
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 27faa7c5c6..5b6c5580ad 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -32,11 +32,10 @@ open Decl_kinds let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr let pr_lident (loc,id) = - if Loc.is_ghost loc then - let (b,_) = Loc.unloc loc in - pr_located pr_id (Loc.make_loc (b,b + String.length(Id.to_string id)),id) - else - pr_id id + match loc with + | None -> pr_id id + | Some loc -> let (b,_) = Loc.unloc loc in + pr_located pr_id @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id let pr_plident (lid, l) = pr_lident lid ++ @@ -50,11 +49,10 @@ open Decl_kinds let pr_fqid fqid = str (string_of_fqid fqid) let pr_lfqid (loc,fqid) = - if Loc.is_ghost loc then - let (b,_) = Loc.unloc loc in - pr_located pr_fqid (Loc.make_loc (b,b + String.length(string_of_fqid fqid)),fqid) - else - pr_fqid fqid + match loc with + | None -> pr_fqid fqid + | Some loc -> let (b,_) = Loc.unloc loc in + pr_located pr_fqid @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (string_of_fqid fqid))) fqid let pr_lname = function | (loc,Name id) -> pr_lident (loc,id) @@ -296,7 +294,7 @@ open Decl_kinds let begin_of_inductive = function | [] -> 0 - | (_,((loc,_),_))::_ -> fst (Loc.unloc loc) + | (_,((loc,_),_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc let pr_class_rawexpr = function | FunClass -> keyword "Funclass" |