X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=fe113743b1d0ef7d9cbe7d2e5b9ccf5cd282c98e;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=d4157677feabd3573bae00edf5c4d84d52795c3d;hpb=6fa89cef6aa8fc1774db065a9fcfc47867579054;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index d4157677f..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 =
@@ -102,7 +104,7 @@ let ask_unsaved parent =
   MatitaGtkMisc.ask_confirmation 
     ~parent ~title:"Unsaved work!" 
     ~message:("Your work is <b>unsaved</b>!\n\n"^
-         "<i>Do you want to save the script before exiting?</i>")
+         "<i>Do you want to save the script before continuing?</i>")
     ()
 
 class gui () =
@@ -137,6 +139,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 +363,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 +577,7 @@ class gui () =
             MatitaLog.error (MatitaExcPp.to_string exn)
           else raise exn);
         (* script *)
+      ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
       let _ =
         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
         | None ->
@@ -605,34 +610,36 @@ class gui () =
               (s ())#saveToFile ();
               console#message ("'"^f^"' saved.\n");
       in
+      let abandon_script () =
+        let status = (s ())#status in
+        if source_view#buffer#modified then
+          (match ask_unsaved main#toplevel with
+          | `YES -> saveScript ()
+          | `NO -> ()
+          | `CANCEL -> raise MatitaTypes.Cancel);
+        (match script_fname with
+        | None -> ()
+        | Some fname -> ask_and_save_moo_if_needed main#toplevel fname status);
+      in
       let loadScript () =
         let script = s () in 
         let status = script#status in
         try 
           match self#chooseFile () with
           | Some f -> 
-                if source_view#buffer#modified then
-                  begin
-                    match ask_unsaved main#toplevel with
-                    | `YES -> saveScript ()
-                    | `NO -> ()
-                    | `CANCEL -> raise MatitaTypes.Cancel
-                  end;
-                (match script_fname with
-                | None -> ()
-                | Some fname -> 
-                    ask_and_save_moo_if_needed main#toplevel fname status);
-                script#reset (); 
-                script#assignFileName f;
-                source_view#source_buffer#begin_not_undoable_action ();
-                script#loadFromFile f; 
-                source_view#source_buffer#end_not_undoable_action ();
-                console#message ("'"^f^"' loaded.\n");
-                self#_enableSaveTo f
+              abandon_script ();
+              script#reset (); 
+              script#assignFileName f;
+              source_view#source_buffer#begin_not_undoable_action ();
+              script#loadFromFile f; 
+              source_view#source_buffer#end_not_undoable_action ();
+              console#message ("'"^f^"' loaded.\n");
+              self#_enableSaveTo f
           | None -> ()
         with MatitaTypes.Cancel -> ()
       in
       let newScript () = 
+        abandon_script ();
         source_view#source_buffer#begin_not_undoable_action ();
         (s ())#reset (); 
         (s ())#template (); 
@@ -695,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 *)
@@ -775,6 +773,58 @@ 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
+      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_find_char Glib.Unichar.isspace)
+          in
+          let ligature = get_ligature last_word 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 *)