latex to unicode in coqide

6 files changed, 131 insertions, 9 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 94778e0c60..5e4994eeb8 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -453,7 +453,7 @@ let compile sn =
     |None -> flash_info "Active buffer has no name"
     |Some f ->
       let args = Coq.get_arguments sn.coqtop in
-      let cmd = cmd_coqc#get 
+      let cmd = cmd_coqc#get
 	^ " " ^ String.concat " " args
 	^ " " ^ (Filename.quote f) ^ " 2>&1"
       in
@@ -766,6 +766,14 @@ let about _ =
   dialog#set_authors authors;
   dialog#show ()
 
+let latex_to_unicode =
+  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*))
+
 let comment = cb_on_current_term (fun t -> t.script#comment ())
 let uncomment = cb_on_current_term (fun t -> t.script#uncomment ())
 
@@ -1161,6 +1169,8 @@ let build_ui () =
       ~callback:MiscMenu.uncomment;
     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;
   ];
 
   menu compile_menu [
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index c994898a4f..c30d6604d2 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -140,6 +140,8 @@ let init () =
 \n    <menuitem action='Uncomment' />\
 \n    <separator />\
 \n    <menuitem action='Coqtop arguments' />\
+\n    <separator />\
+\n    <menuitem action='Latex-to-unicode' />\
 \n  </menu>\
 \n  <menu action='Compile'>\
 \n    <menuitem action='Compile buffer' />\
diff --git a/ide/preferences.ml b/ide/preferences.ml
index fb0eea1405..a5b294cd3a 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -28,6 +28,41 @@ type tag = {
   tag_strikethrough : bool;
 }
 
+
+(** 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
+
 (** Generic preferences *)
 
 type obj = {
@@ -248,6 +283,10 @@ 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_unicode_file =
+  try get_config_file "coqide.bindings"
+  with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) "coqide.bindings"
+
 (** Hooks *)
 
 (** New style preferences *)
@@ -326,7 +365,7 @@ let modifier_for_navigation =
 
 let modifier_for_templates =
   new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string)
- 
+
 let modifier_for_tactics =
   new preference ~name:["modifier_for_tactics"] ~init:"<Control><Alt>" ~repr:Repr.(string)
 
@@ -643,14 +682,15 @@ let save_pref () =
 
 let load_pref () =
   let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in
+  (* TODO: parse loaded_unicode_file and save it in reference latex_to_unicode *)
 
-    let m = Config_lexer.load_file loaded_pref_file in
-    let iter name v =
-      if Util.String.Map.mem name !preferences then
-        try (Util.String.Map.find name !preferences).set v with _ -> ()
-      else unknown_preferences := Util.String.Map.add name v !unknown_preferences
-    in
-    Util.String.Map.iter iter m
+  let m = Config_lexer.load_file loaded_pref_file in
+  let iter name v =
+    if Util.String.Map.mem name !preferences then
+      try (Util.String.Map.find name !preferences).set v with _ -> ()
+    else unknown_preferences := Util.String.Map.add name v !unknown_preferences
+  in
+  Util.String.Map.iter iter m
 
 let pstring name p = string ~f:p#set name p#get
 let pbool name p = bool ~f:p#set name p#get
diff --git a/ide/preferences.mli b/ide/preferences.mli
index cf2265781c..52303ea6cf 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -111,3 +111,5 @@ val stick : 'a preference ->
   (#GObj.widget as 'obj) -> ('a -> unit) -> unit
 
 val use_default_doc_url : string
+
+val get_latex_to_unicode : unit -> (string * string * int option) list
diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 5e26c50797..e407c2a5d8 100644
--- a/ide/wg_ScriptView.ml
+++ b/ide/wg_ScriptView.ml
@@ -10,6 +10,8 @@
 
 open Preferences
 
+exception Abort
+
 type insert_action = {
   ins_val : string;
   ins_off : int;
@@ -405,6 +407,71 @@ 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
+    (** 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, copy-paste from method [comment] above;
+        btw, isn't there a more efficient way to achieve this? *)
+    let rec get_line_start iter =
+      if iter#starts_line then iter
+      else get_line_start iter#backward_char
+      in
+    let buffer = self#buffer in
+    let insert = buffer#get_iter `INSERT in
+    let insert_mark = buffer#create_mark ~left_gravity:false insert in
+    let () = buffer#begin_user_action () in
+    begin try
+      let line_start = get_line_start insert in
+      let prev_backslash_search = insert#backward_search ~limit:line_start "\\" in
+      let backslash =
+        match prev_backslash_search with
+        | None -> raise Abort
+        | Some (backslash_start,backslash_stop) -> backslash_start
+        in
+      let prefix = backslash#get_text ~stop:insert in
+      let word =
+        match lookup prefix with
+        | None ->
+           (* show_warning ("No binding match " ^ prefix); *)
+           raise Abort
+        | Some word -> word
+        in
+      let was_deleted = buffer#delete_interactive ~start:backslash ~stop:insert () in
+      if not was_deleted then raise Abort;
+      let insert2 = buffer#get_iter_at_mark (`MARK insert_mark) in
+      let _was_inserted = buffer#insert_interactive ~iter:insert2 word in
+      ()
+    with Abort -> () end;
+    let () = self#buffer#end_user_action () in
+    self#buffer#delete_mark (`MARK insert_mark)
+
+
   method complete_popup = popup
 
   method undo = undo_manager#undo
diff --git a/ide/wg_ScriptView.mli b/ide/wg_ScriptView.mli
index be6510dbe2..eb1beedfad 100644
--- a/ide/wg_ScriptView.mli
+++ b/ide/wg_ScriptView.mli
@@ -26,6 +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 recenter_insert : unit
   method complete_popup : Wg_Completion.complete_popup
 end