final polishing for coqide bindings

7 files changed, 193 insertions, 156 deletions

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