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

Reviewed-by: ejgallego

3 files changed, 96 insertions, 8 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index fddc294f68..3b36875e3a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -787,25 +787,28 @@ let coqtop_arguments sn =
   let dialog = GWindow.dialog ~title:"Coqtop arguments" () in
   let coqtop = sn.coqtop in
   (* Text entry *)
-  let args = Coq.get_arguments coqtop in
-  let text = String.concat " " args in
+  let text = Ideutils.encode_string_list (Coq.get_arguments coqtop) in
   let entry = GEdit.entry ~text ~packing:dialog#vbox#add () in
   (* Buttons *)
   let box = dialog#action_area in
   let ok = GButton.button ~stock:`OK ~packing:box#add () in
+  let fail s =
+    let msg = Printf.sprintf "Invalid arguments: %s" s in
+    let () = sn.messages#default_route#clear in
+    sn.messages#default_route#push Feedback.Error (Pp.str msg) in
   let ok_cb () =
-    let nargs = String.split_on_char ' ' entry#text in
-    if nargs <> args then
+    let ntext = entry#text in
+    if ntext <> text then
+      match try Util.Inr (Ideutils.decode_string_list ntext) with Failure s -> Util.Inl s with
+      | Util.Inl s -> fail s
+      | Util.Inr nargs ->
       let failed = Coq.filter_coq_opts nargs in
       match failed with
       | [] ->
         let () = Coq.set_arguments coqtop nargs in
         dialog#destroy ()
       | args ->
-        let args = String.concat " " args in
-        let msg = Printf.sprintf "Invalid arguments: %s" args in
-        let () = sn.messages#default_route#clear in
-        sn.messages#default_route#push Feedback.Error (Pp.str msg)
+        fail (String.concat " " args)
     else dialog#destroy ()
   in
   let _ = entry#connect#activate ~callback:ok_cb in
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)
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index b080f5b8ed..9a17eb1402 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