diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-31 17:00:42 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-12-31 17:00:42 +0100 |
| commit | d3bc575c498ae09ad1003405d17a9d5cfbcf3cbf (patch) | |
| tree | 0e4073818b6de4b44e4282bdabf5ab7fb7191072 | |
| parent | b2eaecf0e748e3c286e1ef337f72cee6d3475162 (diff) | |
Do not dump a glob reference when its location is ghost. (Fix bug #4469)
This patch also causes the code to finish a bit faster in the NoGlob case
by not preparing a string for dump_string. It also optimizes
Dumpglob.is_ghost by only checking whether the end position is zero.
Note that no ghost locations were part of the glob files of the standard
library before the patch. Note also that the html documentation of the
standard library is bitwise identical before and after the patch.
| -rw-r--r-- | interp/dumpglob.ml | 7 | ||||
| -rw-r--r-- | lib/loc.ml | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index c18ceecab..c7d3da653 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -139,12 +139,15 @@ let interval loc = loc1, loc2-1 let dump_ref loc filepath modpath ident ty = - if !glob_output = Feedback then + match !glob_output with + | Feedback -> Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty)) - else + | NoGlob -> () + | _ when not (Loc.is_ghost loc) -> let bl,el = interval loc in dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n" bl el filepath modpath ident ty) + | _ -> () let dump_reference loc modpath ident ty = let filepath = Names.DirPath.to_string (Lib.library_dp ()) in diff --git a/lib/loc.ml b/lib/loc.ml index b62677d48..9043bee07 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -31,7 +31,7 @@ let ghost = { fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; bp = 0; ep = 0; } -let is_ghost loc = Pervasives.(=) loc ghost (** FIXME *) +let is_ghost loc = loc.ep = 0 let merge loc1 loc2 = if loc1.bp < loc2.bp then |