diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 41 | ||||
| -rw-r--r-- | printing/pputils.ml | 5 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 20 | ||||
| -rw-r--r-- | printing/prettyp.ml | 16 |
4 files changed, 41 insertions, 41 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index fddd54a9f..900bf2daf 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -147,7 +147,7 @@ let tag_var = tag Tag.variable let pr_with_comments ?loc pp = pr_located (fun x -> x) (Loc.tag ?loc pp) - let pr_sep_com sep f c = pr_with_comments ~loc:(constr_loc c) (sep() ++ f c) + let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c) let pr_univ l = match l with @@ -221,11 +221,10 @@ let tag_var = tag Tag.variable | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t let pr_lident (loc,id) = - if not (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_lname = function | (loc,Name id) -> pr_lident (loc,id) @@ -302,7 +301,7 @@ let tag_var = tag Tag.variable assert false in let loc = cases_pattern_expr_loc (loc, p) in - pr_with_comments ~loc + pr_with_comments ?loc (sep() ++ if prec_less prec inh then strm else surround strm) let pr_patt = pr_patt mt @@ -310,16 +309,18 @@ let tag_var = tag Tag.variable let pr_eqn pr (loc,(pl,rhs)) = let pl = List.map snd pl in spc() ++ hov 4 - (pr_with_comments ~loc + (pr_with_comments ?loc (str "| " ++ hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) - let begin_of_binder = function - | CLocalDef((loc,_),_,_) -> fst (Loc.unloc loc) - | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) - | CLocalPattern(loc,(_,_)) -> fst (Loc.unloc loc) + let begin_of_binder l_bi = + let b_loc l = fst (Option.cata Loc.unloc (0,0) l) in + match l_bi with + | CLocalDef((loc,_),_,_) -> b_loc loc + | CLocalAssum((loc,_)::_,_,_) -> b_loc loc + | CLocalPattern(loc,(_,_)) -> b_loc loc | _ -> assert false let begin_of_binders = function @@ -420,12 +421,12 @@ let tag_var = tag Tag.variable | CLambdaN ((nal,bk,t)::bl,c) -> let bl,c = extract_lam_binders (loc, CLambdaN(bl,c)) in CLocalAssum (nal,bk,t) :: bl, c - | c -> [], Loc.tag ~loc c + | c -> [], Loc.tag ?loc c - let split_lambda = Loc.with_loc (fun ~loc -> function + let split_lambda = Loc.with_loc (fun ?loc -> function | CLambdaN ([[na],bk,t],c) -> (na,t,c) - | CLambdaN (([na],bk,t)::bl,c) -> (na,t,Loc.tag ~loc @@ CLambdaN(bl,c)) - | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t,Loc.tag ~loc @@ CLambdaN((nal,bk,t)::bl,c)) + | CLambdaN (([na],bk,t)::bl,c) -> (na,t,Loc.tag ?loc @@ CLambdaN(bl,c)) + | CLambdaN ((na::nal,bk,t)::bl,c) -> (na,t,Loc.tag ?loc @@ CLambdaN((nal,bk,t)::bl,c)) | _ -> anomaly (Pp.str "ill-formed fixpoint body") ) @@ -436,11 +437,11 @@ let tag_var = tag Tag.variable | (_,Name id), (_,Anonymous) -> (na,t,c) | _ -> (na',t,c) - let split_product na' = Loc.with_loc (fun ~loc -> function + let split_product na' = Loc.with_loc (fun ?loc -> function | CProdN ([[na],bk,t],c) -> rename na na' t c - | CProdN (([na],bk,t)::bl,c) -> rename na na' t (Loc.tag ~loc @@ CProdN(bl,c)) + | CProdN (([na],bk,t)::bl,c) -> rename na na' t (Loc.tag ?loc @@ CProdN(bl,c)) | CProdN ((na::nal,bk,t)::bl,c) -> - rename na na' t (Loc.tag ~loc @@ CProdN((nal,bk,t)::bl,c)) + rename na na' t (Loc.tag ?loc @@ CProdN((nal,bk,t)::bl,c)) | _ -> anomaly (Pp.str "ill-formed fixpoint body") ) @@ -730,7 +731,7 @@ let tag_var = tag Tag.variable return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim) in let loc = constr_loc a in - pr_with_comments ~loc + pr_with_comments ?loc (sep() ++ if prec_less prec inherited then strm else surround strm) type term_pr = { diff --git a/printing/pputils.ml b/printing/pputils.ml index 4ae5035a2..d1ba1a4a1 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -15,14 +15,15 @@ open Locus open Genredexpr let pr_located pr (loc, x) = - if !Flags.beautify && not (Loc.is_ghost loc) then + match loc with + | Some loc when !Flags.beautify -> let (b, e) = Loc.unloc loc in (* Side-effect: order matters *) let before = Pp.comment (CLexer.extract_comments b) in let x = pr x in let after = Pp.comment (CLexer.extract_comments e) in before ++ x ++ after - else pr x + | _ -> pr x let pr_or_var pr = function | ArgArg x -> pr x diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 27faa7c5c..5b6c5580a 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" diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 025514902..eb1124e73 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -711,7 +711,7 @@ let read_sec_context r = let dir = try Nametab.locate_section qid with Not_found -> - user_err ~loc ~hdr:"read_sec_context" (str "Unknown section.") in + user_err ?loc ~hdr:"read_sec_context" (str "Unknown section.") in let rec get_cxt in_cxt = function | (_,Lib.OpenedSection ((dir',_),_) as hd)::rest -> if DirPath.equal dir dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest @@ -752,7 +752,7 @@ let print_any_name = function let print_name = function | ByNotation (loc,(ntn,sc)) -> print_any_name - (Term (Notation.interp_notation_as_global_reference ~loc (fun _ -> true) + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) | AN ref -> print_any_name (locate_any_name ref) @@ -776,11 +776,11 @@ let print_opaque_name qid = | VarRef id -> env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl -let print_about_any loc k = +let print_about_any ?loc k = match k with | Term ref -> let rb = Reductionops.ReductionBehaviour.print ref in - Dumpglob.add_glob loc ref; + Dumpglob.add_glob ?loc ref; pr_infos_list (print_ref false ref :: blankline :: print_name_infos ref @ @@ -789,7 +789,7 @@ let print_about_any loc k = [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> let () = match Syntax_def.search_syntactic_definition kn with - | [],Notation_term.NRef ref -> Dumpglob.add_glob loc ref + | [],Notation_term.NRef ref -> Dumpglob.add_glob ?loc ref | _ -> () in v 0 ( print_syntactic_def kn ++ fnl () ++ @@ -799,11 +799,11 @@ let print_about_any loc k = let print_about = function | ByNotation (loc,(ntn,sc)) -> - print_about_any loc - (Term (Notation.interp_notation_as_global_reference ~loc (fun _ -> true) + print_about_any ?loc + (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) | AN ref -> - print_about_any (loc_of_reference ref) (locate_any_name ref) + print_about_any ?loc:(loc_of_reference ref) (locate_any_name ref) (* for debug *) let inspect depth = |