From 6b88c2d18e6aba570c73aa22299abe1fa3f19039 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 29 Sep 2017 12:25:11 +0200 Subject: Surrounding a few places printing file names with quotes when a space occurs. --- configure.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 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"; -- cgit v1.2.3 From 23f49985296a3594c2cf37fa08e0b3e882d5c9e4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 29 Sep 2017 12:35:01 +0200 Subject: Add a function to surround filenames containing a space with quotes. --- lib/cUnix.ml | 5 +++++ lib/cUnix.mli | 3 +++ 2 files changed, 8 insertions(+) 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..f79f34016a 100644 --- a/lib/cUnix.mli +++ b/lib/cUnix.mli @@ -14,6 +14,9 @@ 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 *) -- cgit v1.2.3 From 0b069d43bd673341f5f115d21b7bb805d485a5ae Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 29 Sep 2017 12:45:17 +0200 Subject: Quote file names which have spaces in "Print LoadPath". The primary concern is for clarity of reading. May it affects tools which would parse the output of "Print LoadPath"? Presumably, these tools would not support file names with spaces already, so this may have no impact. --- vernac/vernacentries.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6191f37080..76a3dc8c2c 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 = -- cgit v1.2.3 From f36ea3ffb4ef01572db437392174f10650bee67b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 29 Sep 2017 12:36:29 +0200 Subject: Unify style of comments in file CUnix. --- lib/cUnix.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/cUnix.mli b/lib/cUnix.mli index f79f34016a..d08dc4c403 100644 --- a/lib/cUnix.mli +++ b/lib/cUnix.mli @@ -19,7 +19,7 @@ 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 @@ -64,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 -- cgit v1.2.3