From 4b694f8a641344875b9076670bc8009476fba4aa Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 23 Feb 2020 13:51:36 +0100
Subject: 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.
---
 ide/ideutils.ml  | 69 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 ide/ideutils.mli | 16 +++++++++++++
 2 files changed, 85 insertions(+)

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
-- 
cgit v1.2.3


From 470f5e063535f91ce0e95798d4aaadfefffb89e0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 23 Feb 2020 14:48:49 +0100
Subject: Use quotes when "necessary" in the coqtop argument window.

This is at least to be able to use spaces in file names (#11595).

In practice it protects also \, ', ", and many other symbols.
---
 ide/coqide.ml | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 553b834a37..2780f27ec3 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
-- 
cgit v1.2.3