support for coqide commande line arguments

5 files changed, 99 insertions, 86 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 5e4994eeb8..bc3f5212f6 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -766,13 +766,9 @@ let about _ =
   dialog#set_authors authors;
   dialog#show ()
 
-let latex_to_unicode =
+let apply_unicode_binding =
   cb_on_current_term (fun t ->
-    (*let show_warning s =
-      t.messages#clear;
-      t.messages#add_string s
-      in*)
-    t.script#latex_to_unicode() (*show_warning*))
+    t.script#apply_unicode_binding())
 
 let comment = cb_on_current_term (fun t -> t.script#comment ())
 let uncomment = cb_on_current_term (fun t -> t.script#uncomment ())
@@ -1170,7 +1166,7 @@ let build_ui () =
     item "Coqtop arguments" ~label:"Coqtop _arguments"
       ~callback:MiscMenu.coqtop_arguments;
     item "Latex-to-unicode" ~label:"_Latex-to-unicode" ~accel:"<Shift>space"
-      ~callback:MiscMenu.latex_to_unicode;
+      ~callback:MiscMenu.apply_unicode_binding;
   ];
 
   menu compile_menu [
@@ -1357,9 +1353,12 @@ let main files =
     this default coqtop path *)
 
 let read_coqide_args argv =
-  let rec filter_coqtop coqtop project_files out = function
+  let rec filter_coqtop coqtop project_files bindings_files out = function
+    |"-unicode-bindings" :: sfilenames :: args ->
+      let filenames = Str.split (Str.regexp ",") sfilenames in
+      filter_coqtop coqtop project_files (filenames @ bindings_files) out args
     |"-coqtop" :: prog :: args ->
-      if coqtop = None then filter_coqtop (Some prog) project_files out args
+      if coqtop = None then filter_coqtop (Some prog) project_files bindings_files out args
       else (output_string stderr "Error: multiple -coqtop options"; exit 1)
     |"-f" :: file :: args ->
       if project_files <> None then
@@ -1367,7 +1366,7 @@ let read_coqide_args argv =
       let d = CUnix.canonical_path_name (Filename.dirname file) in
       let warning_fn x = Format.eprintf "%s@\n%!" x in
       let p = CoqProject_file.read_project_file ~warning_fn file in
-      filter_coqtop coqtop (Some (d,p)) out args
+      filter_coqtop coqtop (Some (d,p)) out bindings_files args
     |"-f" :: [] ->
       output_string stderr "Error: missing project file name"; exit 1
     |"-coqtop" :: [] ->
@@ -1376,19 +1375,21 @@ let read_coqide_args argv =
       Minilib.debug := true;
       Flags.debug := true;
       Backtrace.record_backtrace true;
-      filter_coqtop coqtop project_files ("-debug"::out) args
+      filter_coqtop coqtop project_files bindings_files ("-debug"::out) args
     |"-coqtop-flags" :: flags :: args->
       Coq.ideslave_coqtop_flags := Some flags;
-      filter_coqtop coqtop project_files out args
+      filter_coqtop coqtop project_files bindings_files out args
     |arg::args when out = [] && Minilib.is_prefix_of "-psn_" arg ->
       (* argument added by MacOS during .app launch *)
-      filter_coqtop coqtop project_files out args
-    |arg::args -> filter_coqtop coqtop project_files (arg::out) args
-    |[] -> (coqtop,project_files,List.rev out)
+      filter_coqtop coqtop project_files bindings_files out args
+    |arg::args -> filter_coqtop coqtop project_files bindings_files (arg::out) args
+    |[] -> (coqtop,project_files,bindings_files,List.rev out)
   in
-  let coqtop,project_files,argv = filter_coqtop None None [] argv in
+  let coqtop,project_files,bindings_files,argv = filter_coqtop None None [] [] argv in
+  let bindings_files = if bindings_files = [] then ["default"] else bindings_files in
   Ideutils.custom_coqtop := coqtop;
   custom_project_file := project_files;
+  Preferences.load_unicode_bindings_files bindings_files;
   argv
 
 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 2701089331..57589b4363 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -29,67 +29,6 @@ type tag = {
 }
 
 
-(** 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
-
-    - In case of equality between two candidates (same ascii word, or same
-      priorities for two words with similar prefix), the first binding is considered.
-*)
-
-let latex_to_unicode = ref []
-  (* dummy default, used for testing
-  [
-  ("\\pi", "π", None);
-  ("\\lambdas", "λs", Some 4);
-  ("\\lambda", "λ", Some 3);
-  ("\\lake", "0", Some 2);
-  ("\\lemma", "Lemma foo : x. Proof. Qed", Some 1);
-  ]
-  *)
-
-let get_latex_to_unicode () =
-  !latex_to_unicode
-
-let load_latex_to_unicode_file filename =
-  let acc = ref [] in
-  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
-      acc := (key,value,prio)::!acc;
-      Scanf.Scanning.close_in chline;
-    with End_of_file -> () end;
-  done with End_of_file -> () end;
-  close_in ch;
-  latex_to_unicode := List.rev !acc
-  (*List.iter (fun (x,y,p) ->
-    Printf.eprintf "%s %s %d\n" x y (match p with None -> -1 | Some n -> n))
-   !latex_to_unicode;
-  prerr_newline() *)
-
-
 (** Generic preferences *)
 
 type obj = {
@@ -310,7 +249,7 @@ let loaded_accel_file =
   try get_config_file "coqide.keys"
   with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys"
 
-let loaded_bindings_file =
+let loaded_default_unicode_bindings_file =
   try get_config_file "coqide.bindings"
   with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) "coqide.bindings"
 
@@ -709,7 +648,6 @@ let save_pref () =
 
 let load_pref () =
   let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in
-  let () = load_latex_to_unicode_file loaded_bindings_file in
 
   let m = Config_lexer.load_file loaded_pref_file in
   let iter name v =
@@ -1073,3 +1011,78 @@ 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 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 filenames = List.map (fun f ->
+    if f = "default" then loaded_default_unicode_bindings_file else f) filenames in
+  List.iter process_unicode_bindings_file filenames;
+  unicode_bindings := List.rev !unicode_bindings
+
+  (* For debugging unicode bindings:
+  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()
+  *)
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 52303ea6cf..a75f1b3cec 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -112,4 +112,5 @@ val stick : 'a preference ->
 
 val use_default_doc_url : string
 
-val get_latex_to_unicode : unit -> (string * string * int option) list
+val get_unicode_bindings : unit -> (string * string * int option) list
+val load_unicode_bindings_files : string list -> unit
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 97bf9aefc5..efacaee577 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -407,8 +407,8 @@ object (self)
       self#buffer#delete_mark (`MARK stop_mark)
     | _ -> ()
 
-  method latex_to_unicode () (* (show_warning:string->unit) *) =
-    let bindings = Preferences.get_latex_to_unicode() in
+  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 =
@@ -459,9 +459,7 @@ object (self)
         let prefix = backslash#get_text ~stop:insert in
         let word =
           match lookup prefix with
-          | None ->
-             (* show_warning ("No binding match " ^ prefix); *)
-             raise Abort
+          | None -> raise Abort
           | Some word -> word
           in
         let was_deleted = buffer#delete_interactive ~start:backslash ~stop:insert () in
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index eb1beedfad..ca35b7fb67 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -26,7 +26,7 @@ object
   method set_show_right_margin : bool -> unit
   method comment : unit -> unit
   method uncomment : unit -> unit
-  method latex_to_unicode : unit -> unit (* (string -> unit) -> unit *)
+  method apply_unicode_binding : unit -> unit (* (string -> unit) -> unit *)
   method recenter_insert : unit
   method complete_popup : Wg_Completion.complete_popup
 end