Merge PR #6041: Protecting the printing of filenames with space

4 files changed, 19 insertions, 9 deletions

diff --git a/configure.ml b/configure.ml
index 86f6b7fe38..1ccb691067 100644
--- a/configure.ml
+++ b/configure.ml
@@ -973,6 +973,8 @@ let config_runtime () =
 
 let vmbyteflags = config_runtime ()
 
+let esc s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s
+
 (** * Summary of the configuration *)
 
 let print_summary () =
@@ -985,16 +987,16 @@ let print_summary () =
   pr "  Other bytecode link flags   : %s\n" custom_flag;
   pr "  OS dependent libraries      : %s\n" osdeplibs;
   pr "  OCaml version               : %s\n" caml_version;
-  pr "  OCaml binaries in           : %s\n" camlbin;
-  pr "  OCaml library in            : %s\n" camllib;
+  pr "  OCaml binaries in           : %s\n" (esc camlbin);
+  pr "  OCaml library in            : %s\n" (esc camllib);
   pr "  OCaml flambda flags         : %s\n" (String.concat " " !Prefs.flambda_flags);
   pr "  %s version              : %s\n"     capitalized_camlpX camlpX_version;
-  pr "  %s binaries in          : %s\n"     capitalized_camlpX camlpXbindir;
-  pr "  %s library in           : %s\n"     capitalized_camlpX camlpXlibdir;
+  pr "  %s binaries in          : %s\n"     capitalized_camlpX (esc camlpXbindir);
+  pr "  %s library in           : %s\n"     capitalized_camlpX (esc camlpXlibdir);
   if best_compiler = "opt" then
     pr "  Native dynamic link support : %B\n" hasnatdynlink;
   if coqide <> "no" then
-    pr "  Lablgtk2 library in         : %s\n" !lablgtkdir;
+    pr "  Lablgtk2 library in         : %s\n" (esc !lablgtkdir);
   if !idearchdef = "QUARTZ" then
     pr "  Mac OS integration is on\n";
   pr "  CoqIde                      : %s\n" coqide;
@@ -1009,7 +1011,7 @@ let print_summary () =
   else
     (pr "  Paths for true installation:\n";
      List.iter
-       (fun (_,msg,dir,_) -> pr "  - %s will be copied in %s\n" msg dir)
+       (fun (_,msg,dir,_) -> pr "  - %s will be copied in %s\n" msg (esc dir))
        install_dirs);
   pr "\n";
   pr "If anything is wrong above, please restart './configure'.\n\n";
diff --git a/lib/cUnix.ml b/lib/cUnix.ml
index 867f86a746..34fb660db4 100644
--- a/lib/cUnix.ml
+++ b/lib/cUnix.ml
@@ -14,6 +14,11 @@ type load_path = physical_path list
 let physical_path_of_string s = s
 let string_of_physical_path p = p
 
+let escaped_string_of_physical_path p =
+  (* We assume a reasonable-enough path (typically utf8) and prevents
+     the presence of space; other escapings might be useful... *)
+  if String.contains p ' ' then "\"" ^ p ^ "\"" else p
+
 let path_to_list p =
   let sep = Str.regexp (if Sys.os_type = "Win32" then ";" else ":") in
     Str.split sep p
diff --git a/lib/cUnix.mli b/lib/cUnix.mli
index a394814041..d08dc4c403 100644
--- a/lib/cUnix.mli
+++ b/lib/cUnix.mli
@@ -14,9 +14,12 @@ type load_path = physical_path list
 val physical_path_of_string : string -> physical_path
 val string_of_physical_path : physical_path -> string
 
+(** Escape what has to be escaped (e.g. surround with quotes if with spaces) *)
+val escaped_string_of_physical_path : physical_path -> string
+
 val canonical_path_name : string -> string
 
-(** remove all initial "./" in a path *)
+(** Remove all initial "./" in a path *)
 val remove_path_dot : string -> string
 
 (** If a path [p] starts with the current directory $PWD then
@@ -61,6 +64,6 @@ val sys_command : string -> string list -> Unix.process_status
 
 val waitpid_non_intr : int -> Unix.process_status
 
-(** checks if two file names refer to the same (existing) file *)
+(** Check if two file names refer to the same (existing) file *)
 val same_file : string -> string -> bool
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 62c7edb19d..6a28d701ae 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -153,7 +153,7 @@ let show_match id =
 
 let print_path_entry p =
   let dir = DirPath.print (Loadpath.logical p) in
-  let path = str (Loadpath.physical p) in
+  let path = str (CUnix.escaped_string_of_physical_path (Loadpath.physical p)) in
   Pp.hov 2 (dir ++ spc () ++ path)
 
 let print_loadpath dir =