Adding a function to encode/decode string list into a single string.

This encodes/decodes a list of string into a string in a way
compatible with shell interpretation. On the contrary of
Filename.quote which is for computer consumption, it introduces quotes
for human consumption.

The strategy is to split each string into substrings separated by
simple quotes. Each substring is surrounted by single quotes if it
contains a space. Otherwise, each backslash in the substring is
doubled. The substrings are concatenated separated by
backslash-protected single quote. The strings are then concatenated
separated with spaces. The decoding is shell-like in the sense that it
follows the rules of single quote, backslash and space.

1 files changed, 16 insertions, 0 deletions

diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index af30cd2b05..16467b547f 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -102,3 +102,19 @@ val run_command :
 (* Checks if an error message is printable, it not replaces it with
  * a printable error *)
 val validate : Pp.t -> Pp.t
+
+(** [encode_string_list l] encodes a list of strings into a single
+    string using a "shell"-like encoding: it quotes strings
+    containing space by surrounding them with single quotes, and,
+    outside quoted strings, quotes both single quote and backslash
+    by prefixing them with backslash; the encoding tries to be
+    minimalistic. *)
+
+val encode_string_list : string list -> string
+
+(** [decode_string_list l] decodes the encoding of a string list as
+    a string; it fails with a Failure if a single quote is unmatched
+    or if a backslash in unquoted part is not followed by a single
+    quote or another backslash. *)
+
+val decode_string_list : string -> string list