diff options
| author | Guillaume Melquiond | 2016-06-02 16:11:03 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-06-02 16:13:30 +0200 |
| commit | 9907e296e21fdd9dc3fab2b84fe7159b35af654c (patch) | |
| tree | fc57dc4b3c6827655d3ce691248411838ace628b /toplevel | |
| parent | 2d2d86c165cac7b051da1c5079d614a76550a20c (diff) | |
Remove tabulation support from pretty-printing.
This mechanism relied on functions that are deprecated in recent versions
of ocaml. It was incorrectly used for the most part anyway. The only place
that was using tabulations correctly is "print_loadpath", so there is a
minor regression there: physical paths of short logical paths are no longer
aligned.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 222b7d3df1..65d71c8d51 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -160,7 +160,7 @@ let show_match id = let print_path_entry p = let dir = pr_dirpath (Loadpath.logical p) in let path = str (Loadpath.physical p) in - (dir ++ str " " ++ tbrk (0, 0) ++ path) + Pp.hov 2 (dir ++ spc () ++ path) let print_loadpath dir = let l = Loadpath.get_load_paths () in @@ -170,9 +170,8 @@ let print_loadpath dir = let filter p = is_dirpath_prefix_of dir (Loadpath.logical p) in List.filter filter l in - Pp.t (str "Logical Path: " ++ - tab () ++ str "Physical path:" ++ fnl () ++ - prlist_with_sep fnl print_path_entry l) + str "Logical Path / Physical path:" ++ fnl () ++ + prlist_with_sep fnl print_path_entry l let print_modules () = let opened = Library.opened_libraries () |