X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=fe113743b1d0ef7d9cbe7d2e5b9ccf5cd282c98e;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=dc3fb07cec55ee46627996d934cee317bd8bfd40;hpb=215cb34e905e846d37c873224df1ec30bf81ba87;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index dc3fb07ce..fe113743b 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -29,6 +29,8 @@ open MatitaGeneratedGui
 open MatitaGtkMisc
 open MatitaMisc
 
+exception Found of int
+
 let gui_instance = ref None
 
 class type browserWin =
@@ -575,7 +577,7 @@ class gui () =
             MatitaLog.error (MatitaExcPp.to_string exn)
           else raise exn);
         (* script *)
-      let _ = source_buffer#connect#changed (fun _ -> next_ligatures <- []) in
+      ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
       let _ =
         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
         | None ->
@@ -700,25 +702,16 @@ class gui () =
       connect_button main#scriptRetractButton retract;
       connect_button main#scriptTopButton top;
       connect_button main#scriptBottomButton bottom;
-      connect_key GdkKeysyms._Down advance;
-      connect_key GdkKeysyms._Up retract;
-      connect_key GdkKeysyms._Home top;
-      connect_key GdkKeysyms._End bottom;
       connect_button main#scriptJumpButton jump;
+      connect_menu_item main#scriptAdvanceMenuItem advance;
+      connect_menu_item main#scriptRetractMenuItem retract;
+      connect_menu_item main#scriptTopMenuItem top;
+      connect_menu_item main#scriptBottomMenuItem bottom;
+      connect_menu_item main#scriptJumpMenuItem jump;
       connect_menu_item main#openMenuItem   loadScript;
       connect_menu_item main#saveMenuItem   saveScript;
       connect_menu_item main#saveAsMenuItem saveAsScript;
       connect_menu_item main#newMenuItem    newScript;
-      connect_key GdkKeysyms._period
-        (fun () ->
-          source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
-            ".\n";
-          advance ());
-      connect_key GdkKeysyms._Return
-        (fun () ->
-          source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT)
-            "\n";
-          advance ());
          (* script monospace font stuff *)  
       self#updateFontSize ();
         (* debug menu *)
@@ -786,15 +779,43 @@ class gui () =
         source_buffer#delete ~start:iter ~stop:(iter#copy#backward_chars len);
         source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) s
       in
+      let get_ligature word =
+        let len = String.length word in
+        let aux_tex () =
+          try
+            for i = len - 1 downto 0 do
+              if HExtlib.is_alpha word.[i] then ()
+              else
+                (if word.[i] = '\\' then raise (Found i) else raise (Found ~-1))
+            done;
+            None
+          with Found i ->
+            if i = ~-1 then None else Some (String.sub word i (len - i))
+        in
+        let aux_ligature () =
+          try
+            for i = len - 1 downto 0 do
+              if CicNotationLexer.is_ligature_char word.[i] then ()
+              else raise (Found (i+1))
+            done;
+            raise (Found 0)
+          with
+          | Found i ->
+              (try
+                Some (String.sub word i (len - i))
+              with Invalid_argument _ -> None)
+        in
+        match aux_tex () with
+        | Some macro -> macro
+        | None -> (match aux_ligature () with Some l -> l | None -> word)
+      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
+          let last_word =
+            iter#get_slice
+              ~stop:(iter#copy#backward_find_char Glib.Unichar.isspace)
+          in
+          let ligature = get_ligature last_word in
           (match CicNotationLexer.lookup_ligatures ligature with
           | [] -> ()
           | hd :: tl ->