final polishing for coqide bindings

8 files changed, 198 insertions, 156 deletions

diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index ab7fe2ac08..44955412ce 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -307,6 +307,11 @@ Each of the file tokens provided may consists of one of:
  -  the token ``local``, which resolves to the `coqide.bindings` file
     stored in the user configuration directory.
 
+Remark: if a filename other than the first one includes a "~" to refer
+to the home directory, it won't be expanded properly. To work around that
+issue, one should not use comas but instead repeat the flag, in the form:
+``-unicode-bindings file1 .. -unicode-bindings fileN``.
+
 Remark: if two bindings for a same token both have the same priority value
 (or both have no priority value set), then the binding considered is the
 one from the file that comes first on the command line.
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 8e62ac9193..e16c7db3b4 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1388,7 +1388,7 @@ let read_coqide_args argv =
   let coqtop,project_files,bindings_files,argv = filter_coqtop None None [] [] argv in
   Ideutils.custom_coqtop := coqtop;
   custom_project_file := project_files;
-  Preferences.load_unicode_bindings_files bindings_files;
+  Unicode_bindings.load_files bindings_files;
   argv
 
 
diff --git a/ide/ide.mllib b/ide/ide.mllib
index a7ade71307..f8a2d77be8 100644
--- a/ide/ide.mllib
+++ b/ide/ide.mllib
@@ -11,6 +11,7 @@ Preferences
 Project_file
 Topfmt
 Ideutils
+Unicode_bindings
 Coq
 Coq_lex
 Sentence
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 205961261a..27f240a993 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -249,11 +249,11 @@ let loaded_accel_file =
   try get_config_file "coqide.keys"
   with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys"
 
-let get_bindings_local_file () =
+let get_unicode_bindings_local_file () =
   try Some (get_config_file "coqide.bindings")
   with Not_found -> None
 
-let get_bindings_default_file () =
+let get_unicode_bindings_default_file () =
   let name = "default.bindings" in
   let chk d = Sys.file_exists (Filename.concat d name) in
   try
@@ -1019,124 +1019,3 @@ let configure ?(apply=(fun () -> ())) parent =
   match x with
     | Return_apply | Return_ok -> save_pref ()
     | Return_cancel -> ()
-
-(********************************************************************)
-
-(** Latex to unicode bindings.
-
-    Text description of the unicode bindings, in a file coqide.bindings
-    one item per line, each item consists of:
-    - a leading backslahs
-    - a ascii word next to it
-    - a unicode word (or possibly a full sentence in-between doube-quotes,
-     the sentence may include spaces and \n tokens),
-    - optinally, an integer indicating the "priority" (lower is higher priority),
-      technically the length of the prefix that suffices to obtain this word.
-      Ex. if "\lambda" has priority 3, then "\lam" always decodes as "\lambda".
-
-      \pi π
-      \lambda λ 3
-      \lambdas λs 4
-      \lake Ο 2
-      \lemma "Lemma foo : x. Proof. Qed." 1  ---currently not supported by the parser
-
-    - In case of equality between two candidates (same ascii word, or same
-      priorities for two words with similar prefix), the first binding is considered.
-
-    - Note that if a same token is bound in several bindings file,
-      the one with the lowest priority number will be considered.
-      In case of same priority, the binding from the first loaded file is considered.
-*)
-
-let unicode_bindings = ref []
-  (* example unicode bindings table:
-  [ ("\\pi", "π", None);
-    ("\\lambdas", "λs", Some 4);
-    ("\\lambda", "λ", Some 3);
-    ("\\lake", "0", Some 2);
-    ("\\lemma", "Lemma foo : x. Proof. Qed", Some 1); ] *)
-
-let get_unicode_bindings () =
-  !unicode_bindings
-
-let process_unicode_bindings_file filename =
-  if not (Sys.file_exists filename) then begin
-    output_string stderr (Printf.sprintf "Error: unicode bindings file '%s' was not found.\n" filename); exit 1
-  end;
-  let ch = open_in filename in
-  begin try while true do
-    let line = input_line ch in
-    begin try
-      let chline = Scanf.Scanning.from_string line in
-      let (key,value) =
-        Scanf.bscanf chline "%s %s" (fun x y -> (x,y)) in
-      let prio =
-        try Scanf.bscanf chline " %d" (fun x -> Some x)
-        with Scanf.Scan_failure _ | Failure _ | End_of_file -> None
-        in
-      unicode_bindings := (key,value,prio)::!unicode_bindings;
-      (* Note: storing bindings in reverse order, flipping is done later *)
-      Scanf.Scanning.close_in chline;
-    with End_of_file -> () end;
-  done with End_of_file -> () end;
-  close_in ch
-
-let load_unicode_bindings_files filenames =
-  let selected_filenames = ref [] in
-  let add f =
-    selected_filenames := f::!selected_filenames in
-  if filenames = [] then begin
-    (* If no argument is provided using [-unicode-bindings],
-       then use the default file and the local file, if it exists *)
-    begin match get_bindings_default_file() with
-    | Some f -> add f
-    | None -> output_string stderr (Printf.sprintf "Warning: the file ide/default.bindings was not found in %s.\n" (Envars.coqlib()))
-    (* TODO: flush stderr does not seem to eagerly display the output message *)
-    end;
-    begin match get_bindings_local_file() with
-    | Some f -> add f
-    | None -> ()
-    end;
-  end else begin
-    (* If [-unicode-bindings] is used with a list of file, consider
-       these files in order, with a special treatment for the tokens
-       "default" and "local", which are replaced by the appropriate path. *)
-    let add_arg f =
-      match f with
-      | "default" ->
-        begin match get_bindings_default_file() with
-        | Some f -> add f
-        | None -> output_string stderr (Printf.sprintf "Error:the file ide/default.bindings was not found in %s.\n" (Envars.coqlib())); exit 1
-        end
-      | "local" ->
-        begin match get_bindings_local_file() with
-        | Some f -> add f
-        | None -> output_string stderr (Printf.sprintf "Error: the local configuration file coqide.bindings was not found.\n"); exit 1
-        end
-      | _ -> add f
-      in
-    List.iter add_arg filenames
-  end;
-  (* Files must be processed in order, to build the list of bindings
-     by iteratively consing entry to its head, the list being reversed
-     at the very end *)
-  let real_filenames = List.rev !selected_filenames in
-  List.iter process_unicode_bindings_file real_filenames;
-  unicode_bindings := List.rev !unicode_bindings
-
-  (* For debugging the list of unicode files loaded:
-    List.iter (fun f -> Printf.eprintf "%s\n" f) real_filenames;
-  *)
-  (* For debugging the list of unicode bindings loaded:
-  let print_unicode_bindings () =
-    List.iter (fun (x,y,p) ->
-      Printf.eprintf "%s %s %d\n" x y (match p with None -> -1 | Some n -> n))
-     !unicode_bindings;
-    prerr_newline()
-  *)
-
-  (* TODO: known issue: the "~" in path of several arguments does
-     not seem to be correctly interpreted, e.g.
-       bin/coqide -unicode-bindings local,~/.config/coq/my.bindings &
-     Possible fix is to expand first to absolute paths.
-  *)
diff --git a/ide/preferences.mli b/ide/preferences.mli
index a75f1b3cec..2c505ad180 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -47,6 +47,10 @@ end
 
 val list_tags : unit -> tag preference Util.String.Map.t
 
+val get_unicode_bindings_local_file : unit -> string option
+val get_unicode_bindings_default_file : unit -> string option
+
+
 val cmd_coqtop : string option preference
 val cmd_coqc : string preference
 val cmd_make : string preference
@@ -111,6 +115,3 @@ val stick : 'a preference ->
   (#GObj.widget as 'obj) -> ('a -> unit) -> unit
 
 val use_default_doc_url : string
-
-val get_unicode_bindings : unit -> (string * string * int option) list
-val load_unicode_bindings_files : string list -> unit
diff --git a/ide/unicode_bindings.ml b/ide/unicode_bindings.ml
new file mode 100644
index 0000000000..e2f98302ea
--- /dev/null
+++ b/ide/unicode_bindings.ml
@@ -0,0 +1,131 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+
+let all_bindings = ref []
+  (* example unicode bindings table:
+  [ ("\\pi", "π", None);
+    ("\\lambdas", "λs", Some 4);
+    ("\\lambda", "λ", Some 3);
+    ("\\lake", "0", Some 2);
+    ("\\lemma", "Lemma foo : x. Proof. Qed", Some 1); ] *)
+
+(** Auxiliary function used by [load_files].
+    Takes as argument a valid path. *)
+
+let process_file filename =
+  if not (Sys.file_exists filename) then begin
+    Ideutils.warning (Printf.sprintf "Warning: unicode bindings file '%s' was not found." filename)
+  end else begin
+    let ch = open_in filename in
+    begin try while true do
+      let line = input_line ch in
+      begin try
+        let chline = Scanf.Scanning.from_string line in
+        let (key,value) =
+          Scanf.bscanf chline "%s %s" (fun x y -> (x,y)) in
+        let prio =
+          try Scanf.bscanf chline " %d" (fun x -> Some x)
+          with Scanf.Scan_failure _ | Failure _ | End_of_file -> None
+          in
+        all_bindings := (key,value,prio)::!all_bindings;
+        (* Note: storing bindings in reverse order, flipping is done later *)
+        Scanf.Scanning.close_in chline;
+      with End_of_file -> () end;
+    done with End_of_file -> () end;
+    close_in ch
+  end
+
+let load_files filenames =
+  let selected_filenames = ref [] in
+  let add f =
+    selected_filenames := f::!selected_filenames in
+  let warn_default_not_found () =
+    Ideutils.warning (Printf.sprintf
+      "Warning: the file 'ide/default.bindings' was not found in %s."
+      (Envars.coqlib())) in
+  let warn_local_not_found () =
+    Ideutils.warning (Printf.sprintf
+      "Warning: the local configuration file 'coqide.bindings' was not found.") in
+  if filenames = [] then begin
+    (* If no argument is provided using [-unicode-bindings],
+       then use the default file and the local file, if it exists *)
+    begin match Preferences.get_unicode_bindings_default_file() with
+    | Some f -> add f
+    | None -> warn_default_not_found()
+    end;
+    begin match Preferences.get_unicode_bindings_local_file() with
+    | Some f -> add f
+    | None -> ()
+    end;
+  end else begin
+    (* If [-unicode-bindings] is used with a list of file, consider
+       these files in order, with a special treatment for the tokens
+       "default" and "local", which are replaced by the appropriate path. *)
+    let add_arg f =
+      match f with
+      | "default" ->
+        begin match Preferences.get_unicode_bindings_default_file() with
+        | Some f -> add f
+        | None -> warn_default_not_found()
+        end
+      | "local" ->
+        begin match Preferences.get_unicode_bindings_local_file() with
+        | Some f -> add f
+        | None -> warn_local_not_found()
+        end
+      | _ -> add f
+      in
+    List.iter add_arg filenames
+  end;
+  (* Files must be processed in order, to build the list of bindings
+     by iteratively consing entry to its head, the list being reversed
+     at the very end *)
+  let real_filenames = List.rev !selected_filenames in
+  List.iter process_file real_filenames;
+  all_bindings := List.rev !all_bindings
+  (* For debugging the list of unicode files loaded:
+     List.iter (fun f -> Printf.eprintf "%s\n" f) real_filenames; *)
+
+(** Auxiliary function to test whether [s] is a prefix of [str];
+    Note that there might be overlap with wg_Completion::is_substring *)
+
+let string_is_prefix s str =
+  let n = String.length s in
+  let m = String.length str in
+  if m < n
+    then false
+    else (s = String.sub str 0 n)
+
+let lookup prefix =
+  let max_priority = 100000000 in
+  let cur_word = ref None in
+  let cur_prio = ref (max_priority+1) in
+  let test_binding (key, word, prio_opt) =
+    let prio =
+      match prio_opt with
+      | None -> max_priority
+      | Some p -> p
+      in
+    if string_is_prefix prefix key && prio < !cur_prio then begin
+      cur_word := Some word;
+      cur_prio := prio;
+    end in
+  List.iter test_binding !all_bindings;
+  !cur_word
+
+
+(* For debugging the list of unicode bindings loaded:
+  let print_unicode_bindings () =
+    List.iter (fun (x,y,p) ->
+      Printf.eprintf "%s %s %d\n" x y (match p with None -> -1 | Some n -> n))
+     !all_bindings;
+    prerr_newline()
+*)
diff --git a/ide/unicode_bindings.mli b/ide/unicode_bindings.mli
new file mode 100644
index 0000000000..5b38eeb920
--- /dev/null
+++ b/ide/unicode_bindings.mli
@@ -0,0 +1,48 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+
+(** Latex to unicode bindings.
+    See also the documentation in doc/sphinx/practical-tools/coqide.rst.
+
+    Text description of the unicode bindings, in a file with one item per line,
+    each item consists of:
+    - a leading backslahs
+    - a ascii word next to it
+    - a unicode word (or possibly a full sentence in-between doube-quotes,
+     the sentence may include spaces and \n tokens),
+    - optionally, an integer indicating the "priority" (lower is higher priority),
+      technically the length of the prefix that suffices to obtain this word.
+      Ex. if "\lambda" has priority 3, then "\lam" always decodes as "\lambda".
+
+      \pi π
+      \lambda λ 3
+      \lambdas λs 4
+      \lake Ο 2
+      \lemma "Lemma foo : x. Proof. Qed." 1  ---currently not supported by the parser
+
+    - In case of equality between two candidates (same ascii word, or same
+      priorities for two words with similar prefix), the first binding is considered.
+
+    - Note that if a same token is bound in several bindings file,
+      the one with the lowest priority number will be considered.
+      In case of same priority, the binding from the first file loaded
+      is considered.
+*)
+
+
+(** [load_files] takes a list of filenames and load them as binding files.
+    Filenames may include "default" and "local" as items. *)
+
+val load_files : string list -> unit
+
+(** [lookup] takes a prefix and returns the corresponding unicode value *)
+
+val lookup : string -> string option
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index efacaee577..a3f8aaab25 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -408,34 +408,6 @@ object (self)
     | _ -> ()
 
   method apply_unicode_binding () =
-    let bindings = Preferences.get_unicode_bindings() in
-    (** Auxiliary function to test whether [s] is a prefix of [str];
-        Note that there might be overlap with wg_Completion::is_substring *)
-    let string_is_prefix s str =
-      let n = String.length s in
-      let m = String.length str in
-      if m < n
-        then false
-        else (s = String.sub str 0 n)
-      in
-    (* Auxiliary function to perform the lookup for a binding *)
-    let lookup prefix = (* lookup : string -> string option *)
-      let max_priority = 100000000 in
-      let cur_word = ref None in
-      let cur_prio = ref (max_priority+1) in
-      let test_binding (key, word, prio_opt) =
-        let prio =
-          match prio_opt with
-          | None -> max_priority
-          | Some p -> p
-          in
-        if string_is_prefix prefix key && prio < !cur_prio then begin
-          cur_word := Some word;
-          cur_prio := prio;
-        end in
-      List.iter test_binding bindings;
-      !cur_word
-      in
     (** Auxiliary method to reach the beginning of line or the
         nearest space before the iterator. *)
     let rec get_line_start iter =
@@ -458,7 +430,7 @@ object (self)
           in
         let prefix = backslash#get_text ~stop:insert in
         let word =
-          match lookup prefix with
+          match Unicode_bindings.lookup prefix with
           | None -> raise Abort
           | Some word -> word
           in
@@ -466,6 +438,11 @@ object (self)
         if not was_deleted then raise Abort;
         word
       with Abort -> " "
+       (* Insert a space if no binding applies. This is to make sure that the user
+          gets some visual feedback that the keystroke was taken into account.
+          And also avoid slowing down users who press "Shift" for capitalizing the
+          first letter of a sentence just before typing the "Space" that comes in
+          front of that first letter. *)
       in
     let insert2 = buffer#get_iter_at_mark (`MARK insert_mark) in
     let _was_inserted = buffer#insert_interactive ~iter:insert2 word_to_insert in