diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 7 | ||||
| -rw-r--r-- | printing/pputils.ml | 15 | ||||
| -rw-r--r-- | printing/pputils.mli | 13 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 15 | ||||
| -rw-r--r-- | printing/printing.mllib | 1 |
5 files changed, 40 insertions, 11 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 1d03716d0c..25ea991e7b 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -13,6 +13,7 @@ open Pp open Names open Nameops open Libnames +open Pputils open Ppextend open Constrexpr open Constrexpr_ops @@ -102,7 +103,7 @@ let pr_com_at n = if Flags.do_beautify() && n <> 0 then comment n else mt() -let pr_with_comments loc pp = Loc.pr_located (fun x -> x) (loc,pp) +let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp) let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c) @@ -137,12 +138,12 @@ let pr_opt_type_spc pr = function let pr_lident (loc,id) = if loc <> Loc.ghost then let (b,_) = Loc.unloc loc in - Loc.pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id) + pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id) else pr_id id let pr_lname = function (loc,Name id) -> pr_lident (loc,id) - | lna -> Loc.pr_located pr_name lna + | lna -> pr_located pr_name lna let pr_or_var pr = function | ArgArg x -> pr x diff --git a/printing/pputils.ml b/printing/pputils.ml new file mode 100644 index 0000000000..0c54c61818 --- /dev/null +++ b/printing/pputils.ml @@ -0,0 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp + +let pr_located pr (loc, x) = + if Flags.do_beautify () && loc <> Loc.ghost then + let (b, e) = Loc.unloc loc in + Pp.comment b ++ pr x ++ Pp.comment e + else pr x diff --git a/printing/pputils.mli b/printing/pputils.mli new file mode 100644 index 0000000000..bac2815faf --- /dev/null +++ b/printing/pputils.mli @@ -0,0 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp + +val pr_located : ('a -> std_ppcmds) -> 'a Loc.located -> std_ppcmds +(** Prints an object surrounded by its commented location *) + diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 748e5297b2..3553373fb7 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -9,13 +9,12 @@ open Pp open Names -let pr_located = Loc.pr_located - -open Compat +(* open Compat *) open Errors open Util open Extend open Vernacexpr +open Pputils open Ppconstr open Pptactic open Libnames @@ -28,8 +27,8 @@ let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr let pr_lident (loc,id) = if loc <> Loc.ghost then - let (b,_) = unloc loc in - pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) + let (b,_) = Loc.unloc loc in + pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id) else pr_id id let string_of_fqid fqid = @@ -39,8 +38,8 @@ let pr_fqid fqid = str (string_of_fqid fqid) let pr_lfqid (loc,fqid) = if loc <> Loc.ghost then - let (b,_) = unloc loc in - pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid) + 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 @@ -319,7 +318,7 @@ let pr_onescheme (idop,schem) = let begin_of_inductive = function [] -> 0 - | (_,((loc,_),_))::_ -> fst (unloc loc) + | (_,((loc,_),_))::_ -> fst (Loc.unloc loc) let pr_class_rawexpr = function | FunClass -> str"Funclass" diff --git a/printing/printing.mllib b/printing/printing.mllib index 2de798aa45..6d6e1bba67 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -1,3 +1,4 @@ +Pputils Ppconstr Printer Pptactic |