aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
authorHugo Herbelin2020-02-23 13:51:36 +0100
committerHugo Herbelin2020-03-15 08:30:40 +0100
commit4b694f8a641344875b9076670bc8009476fba4aa (patch)
treedcdfe889c1287df5b66bfa761ef9403f0413fcf9 /ide
parent1f984236f4bdc441b80f19bcc32424a45d8168f3 (diff)
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.
Diffstat (limited to 'ide')
-rw-r--r--ide/ideutils.ml69
-rw-r--r--ide/ideutils.mli16
2 files changed, 85 insertions, 0 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 38da229d61..c21be68b63 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -536,3 +536,72 @@ let rec is_valid (s : Pp.t) = match Pp.repr s with
| Pp.Ppcmd_comment s -> List.for_all Glib.Utf8.validate s
let validate s =
if is_valid s then s else Pp.str "This error massage can't be printed."
+
+(** encoding list of strings as a string in a shell-like compatible way:
+ string with spaces and no ' -> '...'
+ string with spaces and ' -> split string into substrings separated with \'
+ ' -> \'
+ \ -> \\
+ *)
+
+let decode_string_list s =
+ let l = String.length s in
+ let fail_backslash () =
+ failwith "Backslash is used to quote single quotes in quoted strings; it should otherwise be doubled" in
+ let rec find_word quoted b i =
+ if i = l then
+ if quoted then failwith "Unmatched single quote"
+ else i
+ else
+ let c = s.[i] in
+ if c = ' ' && not quoted then i+1
+ else if c = '\'' then find_word (not quoted) b (i+1)
+ else if c = '\\' && not quoted then
+ if i = l-1 then fail_backslash ()
+ else
+ let c = s.[i+1] in
+ if c = '\'' || c = '\\' then
+ (Buffer.add_char b c; find_word quoted b (i+2))
+ else fail_backslash ()
+ else
+ (Buffer.add_char b c;
+ find_word quoted b (i+1)) in
+ let rec collect_words i =
+ if i = l then [] else
+ let b = Buffer.create l in
+ let i = find_word false b i in
+ Buffer.contents b :: collect_words i in
+ collect_words 0
+
+let needs_quote s i =
+ (* Tells if there is a space and if a space, before the next single quote *)
+ match CString.index_from_opt s i ' ', CString.index_from_opt s i '\'' with
+ | Some _, None -> true
+ | Some i, Some j -> i < j
+ | _ -> false
+
+let encode_string s =
+ (* Could be optimized so that "a b'c" is "'a b'\'c" rather than "'a b'\''c'" *)
+ let l = String.length s in
+ let b = Buffer.create (l + 10) in
+ let close quoted = if quoted then Buffer.add_char b '\'' in
+ let rec aux quoted i =
+ if i = l then close quoted
+ else
+ let c = s.[i] in
+ if c = '\'' then
+ (close quoted;
+ Buffer.add_string b "\\'";
+ start (i+1))
+ else if c = '\\' && not quoted then
+ (Buffer.add_string b "\\\\"; aux quoted (i+1))
+ else
+ (Buffer.add_char b c; aux quoted (i+1))
+ and start i =
+ let q = needs_quote s i in
+ if q then Buffer.add_char b '\'';
+ aux q i in
+ start 0;
+ Buffer.contents b
+
+let encode_string_list l = String.concat " " (List.map encode_string l)
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