diff options
| author | Hugo Herbelin | 2020-02-23 13:51:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-15 08:30:40 +0100 |
| commit | 4b694f8a641344875b9076670bc8009476fba4aa (patch) | |
| tree | dcdfe889c1287df5b66bfa761ef9403f0413fcf9 /ide | |
| parent | 1f984236f4bdc441b80f19bcc32424a45d8168f3 (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.ml | 69 | ||||
| -rw-r--r-- | ide/ideutils.mli | 16 |
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 |
