added support for expansion of ligatures ALT-L will trigger it

[helm.git] / helm / matita / matitaGui.ml

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 589da7dcc8e9adb6eed32d161a7b9b583ec23b33..dc3fb07cec55ee46627996d934cee317bd8bfd40 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -137,6 +137,7 @@ class gui () =
     val mutable script_fname = None
     val mutable font_size = default_font_size
     val mutable next_devel_must_contain = None
+    val mutable next_ligatures = []
    
     initializer
         (* glade's check widgets *)
@@ -360,6 +361,7 @@ class gui () =
         source_buffer#move_mark `SEL_BOUND source_buffer#end_iter);
       connect_menu_item main#findReplMenuItem show_find_Repl;
       connect_menu_item main#externalEditorMenuItem self#externalEditor;
+      connect_menu_item main#ligatureButton self#nextLigature;
       ignore (findRepl#findEntry#connect#activate find_forward);
         (* interface lockers *)
       let lock_world _ =
@@ -573,6 +575,7 @@ class gui () =
             MatitaLog.error (MatitaExcPp.to_string exn)
           else raise exn);
         (* script *)
+      let _ = source_buffer#connect#changed (fun _ -> next_ligatures <- []) in
       let _ =
         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
         | None ->
@@ -777,6 +780,30 @@ class gui () =
         MatitaMathView.update_font_sizes ());
       MatitaMathView.reset_font_size ();
     
+    method private nextLigature () =
+      let iter = source_buffer#get_iter_at_mark `INSERT in
+      let write_ligature len s =
+        source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars len);
+        source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s
+      in
+      (match next_ligatures with
+      | [] -> (* find ligatures and fill next_ligatures, then try again *)
+          let last_word = iter#get_slice ~stop:iter#copy#backward_word_start in
+          let len = String.length last_word in
+          let i = ref (len - 1) in
+          while !i >= 0 && CicNotationLexer.is_ligature_char last_word.[!i] do
+            decr i
+          done;
+          let ligature = String.sub last_word (!i + 1) (len - (!i + 1)) in
+          (match CicNotationLexer.lookup_ligatures ligature with
+          | [] -> ()
+          | hd :: tl ->
+              write_ligature (String.length ligature) hd;
+              next_ligatures <- tl @ [ hd ])
+      | hd :: tl ->
+          write_ligature 1 hd;
+          next_ligatures <- tl @ [ hd ])
+
     method private externalEditor () =
       let cmd = Helm_registry.get "matita.external_editor" in
 (* ZACK uncomment to enable interactive ask of external editor command *)