Merge PR #11664: Encoding string list as a string with application to the parsing of coqtop arguments in coqide

Reviewed-by: ejgallego

1 files changed, 69 insertions, 0 deletions

diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index eeb818ce5f..482cecc1f8 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)