diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-02-20 16:01:29 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-02-20 16:01:29 +0100 |
| commit | 2b4f249ed0a28cde876f18aacf19f646d8af8fae (patch) | |
| tree | 785019647a01b9eaa0e662e08422df294ebb8dca /vernac/vernacentries.ml | |
| parent | 278cebe6835512a5646eafcb13e1f020c0dc5d91 (diff) | |
| parent | 9907e296e21fdd9dc3fab2b84fe7159b35af654c (diff) | |
Merge PR#189: Remove tabulation support from pretty-printing.
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0bf81e7e5..8b7d65457 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -165,7 +165,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 @@ -175,9 +175,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 () |