1 files changed, 54 insertions, 9 deletions

diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml
index 5e26c50797..8802eb0f1c 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;
@@ -284,12 +286,12 @@ end
 
 class script_view (tv : source_view) (ct : Coq.coqtop) =
 
-let view = new GSourceView2.source_view (Gobject.unsafe_cast tv) in
+let view = new GSourceView3.source_view (Gobject.unsafe_cast tv) in
 let completion = new Wg_Completion.complete_model ct view#buffer in
 let popup = new Wg_Completion.complete_popup completion (view :> GText.view) in
 
 object (self)
-  inherit GSourceView2.source_view (Gobject.unsafe_cast tv)
+  inherit GSourceView3.source_view (Gobject.unsafe_cast tv)
 
   val undo_manager = new undo_manager view#buffer
 
@@ -405,6 +407,49 @@ object (self)
       self#buffer#delete_mark (`MARK stop_mark)
     | _ -> ()
 
+  method apply_unicode_binding () =
+    (* Auxiliary method to reach the beginning of line or the
+        nearest space before the iterator. *)
+    let rec get_line_start iter =
+      if iter#starts_line || Glib.Unichar.isspace iter#char then iter
+      else get_line_start iter#backward_char
+      in
+    (* Main action *)
+    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
+    let word_to_insert =
+      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 Unicode_bindings.lookup prefix with
+          | None -> raise Abort
+          | Some word -> word
+          in
+        let was_deleted = buffer#delete_interactive ~start:backslash ~stop:insert () in
+        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
+    let () = self#buffer#end_user_action () in
+    self#buffer#delete_mark (`MARK insert_mark)
+
+
   method complete_popup = popup
 
   method undo = undo_manager#undo
@@ -461,7 +506,7 @@ object (self)
     in
     let _ = GtkSignal.connect ~sgn:move_line_signal ~callback obj in
     (* Plug on preferences *)
-    let cb clr = self#misc#modify_base [`NORMAL, `NAME clr] in
+    let cb clr = self#misc#modify_bg [`NORMAL, `NAME clr] in
     let _ = background_color#connect#changed ~callback:cb in
     let _ = self#misc#connect#realize ~callback:(fun () -> cb background_color#get) in
 
@@ -484,24 +529,24 @@ object (self)
     stick tab_length self self#set_tab_width;
     stick auto_complete self self#set_auto_complete;
 
-    let cb ft = self#misc#modify_font (Pango.Font.from_string ft) in
+    let cb ft = self#misc#modify_font (GPango.font_description_from_string ft) in
     stick text_font self cb;
 
     ()
 
 end
 
-let script_view ct ?(source_buffer:GSourceView2.source_buffer option)  ?draw_spaces =
-  GtkSourceView2.SourceView.make_params [] ~cont:(
+let script_view ct ?(source_buffer:GSourceView3.source_buffer option)  ?draw_spaces =
+  GtkSourceView3.SourceView.make_params [] ~cont:(
     GtkText.View.make_params ~cont:(
       GContainer.pack_container ~create:
 	(fun pl ->
 	  let w = match source_buffer with
-	    | None -> GtkSourceView2.SourceView.new_ ()
-	    | Some buf -> GtkSourceView2.SourceView.new_with_buffer
+            | None -> GtkSourceView3.SourceView.new_ ()
+            | Some buf -> GtkSourceView3.SourceView.new_with_buffer
               (Gobject.try_cast buf#as_buffer "GtkSourceBuffer")
 	  in
 	  let w = Gobject.unsafe_cast w in
 	  Gobject.set_params (Gobject.try_cast w "GtkSourceView") pl;
-	  Gaux.may ~f:(GtkSourceView2.SourceView.set_draw_spaces w) draw_spaces;
+          Gaux.may ~f:(GtkSourceView3.SourceView.set_draw_spaces w) draw_spaces;
 	  ((new script_view w ct) : script_view))))