diff options
author | 2012-06-22 15:14:30 +0000 | |
---|---|---|
committer | 2012-06-22 15:14:30 +0000 | |
commit | 6b45f2d36929162cf92272bb60c2c245d9a0ead3 (patch) | |
tree | 93aa975697b7de73563c84773d99b4c65b92173b /lib/pp.ml4 | |
parent | fea214f82954197d23fda9a0e4e7d93e0cbf9b4c (diff) |
Added an indirection with respect to Loc in Compat. As many [open Compat]
were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.
This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/pp.ml4')
-rw-r--r-- | lib/pp.ml4 | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 789de8160..fb85af0eb 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -7,7 +7,6 @@ (************************************************************************) open Pp_control -open Compat (* This should not be used outside of this file. Use Flags.print_emacs instead. This one is updated when reading @@ -374,19 +373,6 @@ let string_of_ppcmds c = msg_with Format.str_formatter c; Format.flush_str_formatter () -(* Locations management *) -type loc = Loc.t -let dummy_loc = Loc.ghost -let join_loc = Loc.merge -let make_loc = make_loc -let unloc = unloc - -type 'a located = loc * 'a -let located_fold_left f x (_,a) = f x a -let located_iter2 f (_,a) (_,b) = f a b -let down_located f (_,a) = f a - - (* Copy paste from Util *) let pr_comma () = str "," ++ spc () @@ -467,10 +453,4 @@ let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v let prvect elem v = prvect_with_sep mt elem v -let pr_located pr (loc,x) = - if Flags.do_beautify() && loc<>dummy_loc then - let (b,e) = unloc loc in - comment b ++ pr x ++ comment e - else pr x - let surround p = hov 1 (str"(" ++ p ++ str")") |