X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=cf141722992e3d49ccba720beba267d0396867d7;hb=5c56a926588a63ceac31e6ddd6e3eeb02fadf3a9;hp=ac69d2615a902bc822ff656a8a4dcbe543a289a0;hpb=8df7fb956e77d5863338587ac3fdd5f46669d331;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index ac69d2615..cf1417229 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -29,7 +29,7 @@ open MatitaGeneratedGui
 open MatitaGtkMisc
 open MatitaMisc
 
-let gui_instance = ref None ;;
+let gui_instance = ref None
 
 class type browserWin =
   (* this class exists only because GEdit.combo_box_entry is not supported by
@@ -107,11 +107,10 @@ let ask_unsaved parent =
 class gui () =
     (* creation order _is_ relevant for windows placement *)
   let main = new mainWin () in
-  let about = new aboutWin () in
   let fileSel = new fileSelectionWin () in
   let findRepl = new findReplWin () in
   let develList = new develListWin () in
-  let newDevel = new newDevelopmentWin () in
+  let newDevel = new newDevelWin () in
   let keyBindingBoxes = (* event boxes which should receive global key events *)
     [ main#mainWinEventBox ]
   in
@@ -130,6 +129,11 @@ class gui () =
       ~default:BuildTimeConf.default_font_size "matita.font_size"
   in
   let source_buffer = source_view#source_buffer in
+(*   let _ =
+    source_view#event#connect#selection_clear (fun _ ->
+      prerr_endline "source_view: selection clear";
+      false)
+  in *)
   object (self)
     val mutable chosen_file = None
     val mutable _ok_not_exists = false
@@ -142,7 +146,7 @@ class gui () =
         (* glade's check widgets *)
       List.iter (fun w -> w#check_widgets ())
         (let c w = (w :> <check_widgets: unit -> unit>) in
-        [ c about; c fileSel; c main; c findRepl]);
+        [ c fileSel; c main; c findRepl]);
         (* key bindings *)
       List.iter (* global key bindings *)
         (fun (key, callback) -> self#addKeyBinding key callback)
@@ -154,13 +158,32 @@ class gui () =
 *)
         [ ];
         (* about win *)
-      ignore (about#aboutWin#event#connect#delete (fun _ -> true));
-      ignore (main#aboutMenuItem#connect#activate (fun _ ->
-        about#aboutWin#show ()));
-      connect_button about#aboutDismissButton (fun _ ->
-        about#aboutWin#misc#hide ());
-      about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
-        ~templ:BuildTimeConf.version about#aboutLabel#label);
+      let parse_txt_file file =
+       let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in
+       let l_rev = ref [] in
+       try
+        while true do
+         l_rev := input_line ch :: !l_rev;
+        done;
+        assert false
+       with
+        End_of_file ->
+         close_in ch;
+         List.rev !l_rev in 
+      let about_dialog =
+       GWindow.about_dialog
+        ~authors:(parse_txt_file "AUTHORS")
+        (*~comments:"comments"*)
+        ~copyright:"Copyright (C) 2005, the HELM team"
+        ~license:(String.concat "\n" (parse_txt_file "LICENSE"))
+        (*?logo:GdkPixbuf.pixbuf*)
+        (*?logo_icon_name:string*)
+        ~name:"Matita"
+        ~version:BuildTimeConf.version
+        ~website:"http://helm.cs.unibo.it"
+        ()
+      in
+      connect_menu_item main#aboutMenuItem about_dialog#present;
         (* findRepl win *)
       let show_find_Repl () = 
         findRepl#toplevel#misc#show ();
@@ -197,9 +220,172 @@ class gui () =
       connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ());
       ignore(findRepl#toplevel#event#connect#delete 
         ~callback:(fun _ -> hide_find_Repl ();true));
-      ignore(self#main#findReplMenuItem#connect#activate
-        ~callback:show_find_Repl);
-      ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
+      let safe_undo =
+       fun () ->
+        (* phase 1: we save the actual status of the marks and we undo *)
+        let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in
+        let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
+        let locked_iter_offset = locked_iter#offset in
+        let mark2 =
+         `MARK
+           (source_view#buffer#create_mark ~name:"lock_point"
+             ~left_gravity:true locked_iter) in
+        source_view#source_buffer#undo ();
+        (* phase 2: we save the cursor position and we redo, restoring
+           the previous status of all the marks *)
+        let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
+        let mark =
+         `MARK
+           (source_view#buffer#create_mark ~name:"undo_point"
+             ~left_gravity:true cursor_iter)
+        in
+         source_view#source_buffer#redo ();
+         let mark_iter = source_view#buffer#get_iter_at_mark mark in
+         let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
+         let mark2_iter = mark2_iter#set_offset locked_iter_offset in
+          source_view#buffer#move_mark locked_mark ~where:mark2_iter;
+          source_view#buffer#delete_mark mark;
+          source_view#buffer#delete_mark mark2;
+          (* phase 3: if after the undo the cursor was in the locked area,
+             then we move it there again and we perform a goto *)
+          if mark_iter#offset < locked_iter_offset then
+           begin
+            source_view#buffer#move_mark `INSERT ~where:mark_iter;
+            (MatitaScript.instance ())#goto `Cursor ();
+           end;
+          (* phase 4: we perform again the undo. This time we are sure that
+             the text to undo is not locked *)
+          source_view#source_buffer#undo ();
+          source_view#misc#grab_focus () in
+      let safe_redo =
+       fun () ->
+        (* phase 1: we save the actual status of the marks, we redo and
+           we undo *)
+        let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in
+        let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
+        let locked_iter_offset = locked_iter#offset in
+        let mark2 =
+         `MARK
+           (source_view#buffer#create_mark ~name:"lock_point"
+             ~left_gravity:true locked_iter) in
+        source_view#source_buffer#redo ();
+        source_view#source_buffer#undo ();
+        (* phase 2: we save the cursor position and we restore
+           the previous status of all the marks *)
+        let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
+        let mark =
+         `MARK
+           (source_view#buffer#create_mark ~name:"undo_point"
+             ~left_gravity:true cursor_iter)
+        in
+         let mark_iter = source_view#buffer#get_iter_at_mark mark in
+         let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
+         let mark2_iter = mark2_iter#set_offset locked_iter_offset in
+          source_view#buffer#move_mark locked_mark ~where:mark2_iter;
+          source_view#buffer#delete_mark mark;
+          source_view#buffer#delete_mark mark2;
+          (* phase 3: if after the undo the cursor is in the locked area,
+             then we move it there again and we perform a goto *)
+          if mark_iter#offset < locked_iter_offset then
+           begin
+            source_view#buffer#move_mark `INSERT ~where:mark_iter;
+            (MatitaScript.instance ())#goto `Cursor ();
+           end;
+          (* phase 4: we perform again the redo. This time we are sure that
+             the text to redo is not locked *)
+          source_view#source_buffer#redo ();
+          source_view#misc#grab_focus ()
+      in
+      connect_menu_item main#undoMenuItem safe_undo;
+      ignore(source_view#source_buffer#connect#can_undo
+        ~callback:main#undoMenuItem#misc#set_sensitive);
+      connect_menu_item main#redoMenuItem safe_redo;
+      ignore(source_view#source_buffer#connect#can_redo
+        ~callback:main#redoMenuItem#misc#set_sensitive);
+      ignore(source_view#connect#after#populate_popup
+       ~callback:(fun pre_menu ->
+         let menu = new GMenu.menu pre_menu in
+         let menuItems = menu#children in
+         let undoMenuItem, redoMenuItem =
+          match menuItems with
+             [undo;redo;sep1;cut;copy;paste;delete;sep2;
+              selectall;sep3;inputmethod;insertunicodecharacter] -> undo,redo
+           | _ -> assert false in
+         let new_undoMenuItem =
+          GMenu.image_menu_item
+           ~image:(GMisc.image ~stock:`UNDO ())
+           ~use_mnemonic:true
+           ~label:"_Undo"
+           ~packing:(menu#insert ~pos:0) () in
+         new_undoMenuItem#misc#set_sensitive
+          (undoMenuItem#misc#get_flag `SENSITIVE);
+         menu#remove (undoMenuItem :> GMenu.menu_item);
+         connect_menu_item new_undoMenuItem safe_undo;
+         let new_redoMenuItem =
+          GMenu.image_menu_item
+           ~image:(GMisc.image ~stock:`REDO ())
+           ~use_mnemonic:true
+           ~label:"_Redo"
+           ~packing:(menu#insert ~pos:1) () in
+         new_redoMenuItem#misc#set_sensitive
+          (redoMenuItem#misc#get_flag `SENSITIVE);
+          menu#remove (redoMenuItem :> GMenu.menu_item);
+          connect_menu_item new_redoMenuItem safe_redo));
+      let clipboard = GData.clipboard Gdk.Atom.clipboard in
+      let text_selected () =
+        (source_buffer#get_iter_at_mark `INSERT)#compare
+          (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
+      in
+      let markup_selected () = MatitaMathView.get_selections () <> None in
+      connect_menu_item main#editMenu (fun () ->
+        let text_selected = text_selected () in
+        let markup_selected = markup_selected () in
+        let something_selected = text_selected || markup_selected in
+        main#cutMenuItem#misc#set_sensitive text_selected;
+        main#copyMenuItem#misc#set_sensitive something_selected;
+        main#deleteMenuItem#misc#set_sensitive text_selected;
+        main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None));
+      connect_menu_item main#cutMenuItem (fun () ->
+        source_view#buffer#cut_clipboard clipboard);
+      connect_menu_item main#copyMenuItem (fun () ->
+        if text_selected () then
+          source_view#buffer#copy_clipboard clipboard
+        else if markup_selected () then
+          match MatitaMathView.get_selections () with
+          | None
+          | Some [] -> ()
+          | Some (s :: _) -> clipboard#set_text s);
+      connect_menu_item main#pasteMenuItem (fun () ->
+        source_view#buffer#paste_clipboard clipboard;
+        (MatitaScript.instance ())#clean_dirty_lock);
+      connect_menu_item main#deleteMenuItem (fun () ->
+        ignore (source_view#buffer#delete_selection ()));
+      connect_menu_item main#selectAllMenuItem (fun () ->
+        source_buffer#move_mark `INSERT source_buffer#start_iter;
+        source_buffer#move_mark `SEL_BOUND source_buffer#end_iter);
+      connect_menu_item main#findReplMenuItem show_find_Repl;
+      ignore (findRepl#findEntry#connect#activate find_forward);
+        (* interface lockers *)
+      let lock_world _ =
+        main#buttonsToolbar#misc#set_sensitive false;
+        develList#buttonsHbox#misc#set_sensitive false;
+        source_view#set_editable false
+      in
+      let unlock_world _ =
+        main#buttonsToolbar#misc#set_sensitive true;
+        develList#buttonsHbox#misc#set_sensitive true;
+        source_view#set_editable true
+      in
+      let locker f = 
+        fun () -> 
+          lock_world ();
+          try f ();unlock_world () with exc -> unlock_world (); raise exc in
+      let keep_focus f =
+        fun () ->
+         try
+          f (); source_view#misc#grab_focus ()
+         with
+          exc -> source_view#misc#grab_focus (); raise exc in
         (* developments win *)
       let model = 
         new MatitaGtkMisc.multiStringListModel 
@@ -216,37 +402,45 @@ class gui () =
         | [[name;_]] -> MatitamakeLib.development_for_name name
         | _ -> assert false 
       in
+      let refresh () = 
+        while Glib.Main.pending () do 
+          ignore(Glib.Main.iteration false); 
+        done
+      in
       connect_button develList#newButton
         (fun () -> 
           next_devel_must_contain <- None;
           newDevel#toplevel#misc#show());
       connect_button develList#deleteButton
-        (fun () -> 
+        (locker (fun () -> 
           (match get_devel_selected () with
           | None -> ()
-          | Some d -> MatitamakeLib.destroy_development d);
-          refresh_devels_win ());
-      let refresh () = 
-        while Glib.Main.pending () do 
-          ignore(Glib.Main.iteration false); 
-        done
-      in
+          | Some d -> MatitamakeLib.destroy_development_in_bg refresh d);
+          refresh_devels_win ()));
       connect_button develList#buildButton 
-        (fun () -> 
+        (locker (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d));
+          | Some d -> 
+              let build = locker 
+                (fun () -> MatitamakeLib.build_development_in_bg refresh d)
+              in
+              ignore(build ())));
       connect_button develList#cleanButton 
-        (fun () -> 
+        (locker (fun () -> 
           match get_devel_selected () with
           | None -> ()
-          | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
+          | Some d -> 
+              let clean = locker 
+                (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
+              in
+              ignore(clean ())));
       connect_button develList#closeButton 
         (fun () -> develList#toplevel#misc#hide());
       ignore(develList#toplevel#event#connect#delete 
         (fun _ -> develList#toplevel#misc#hide();true));
       let selected_devel = ref None in
-      connect_menu_item self#main#developmentsMenuItem
+      connect_menu_item main#developmentsMenuItem
         (fun () -> refresh_devels_win ();develList#toplevel#misc#show ());
       
         (* add development win *)
@@ -321,7 +515,6 @@ class gui () =
         | `DELETE_EVENT -> return None));
         (* menus *)
       List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
-      main#helpMenu#set_right_justified true;
         (* console *)
       let adj = main#logScrolledWin#vadjustment in
         ignore (adj#connect#changed
@@ -343,7 +536,7 @@ class gui () =
           buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked"))
             ("\n" ^ GrafiteAstPp.pp_tactic ast)
       in
-      let tbar = self#main in
+      let tbar = main in
       connect_button tbar#introsButton (tac (A.Intros (loc, None, [])));
       connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole)));
       connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole)));
@@ -359,21 +552,21 @@ class gui () =
         (tac_w_term (A.Transitivity (loc, hole)));
       connect_button tbar#assumptionButton (tac (A.Assumption loc));
       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
-      connect_button tbar#autoButton (tac (A.Auto (loc,None,None)));
+      connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None))); (* ALB *)
       MatitaGtkMisc.toggle_widget_visibility
-       ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
-       ~check:self#main#tacticsBarMenuItem;
+       ~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
+       ~check:main#tacticsBarMenuItem;
       let module Hr = Helm_registry in
       if
         not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar")
       then 
-        self#main#tacticsBarMenuItem#set_active false;
+        main#tacticsBarMenuItem#set_active false;
       MatitaGtkMisc.toggle_callback 
         ~callback:(function 
-          | true -> self#main#toplevel#fullscreen () 
-          | false -> self#main#toplevel#unfullscreen ())
-        ~check:self#main#fullscreenMenuItem;
-      self#main#fullscreenMenuItem#set_active false;
+          | true -> main#toplevel#fullscreen () 
+          | false -> main#toplevel#unfullscreen ())
+        ~check:main#fullscreenMenuItem;
+      main#fullscreenMenuItem#set_active false;
         (* log *)
       MatitaLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=
@@ -391,7 +584,7 @@ class gui () =
       let s () = MatitaScript.instance () in
       let disableSave () =
         script_fname <- None;
-        self#main#saveMenuItem#misc#set_sensitive false
+        main#saveMenuItem#misc#set_sensitive false
       in
       let saveAsScript () =
         let script = s () in
@@ -431,7 +624,7 @@ class gui () =
                 script#reset (); 
                 script#assignFileName f;
                 source_view#source_buffer#begin_not_undoable_action ();
-                script#loadFromFile (); 
+                script#loadFromFile f; 
                 source_view#source_buffer#end_not_undoable_action ();
                 console#message ("'"^f^"' loaded.\n");
                 self#_enableSaveTo f
@@ -448,33 +641,19 @@ class gui () =
       in
       let cursor () =
         source_buffer#place_cursor
-          (source_buffer#get_iter_at_mark (`NAME "locked"))
-      in
-      let lock_world _ =
-        main#buttonsToolbar#misc#set_sensitive false;
-        source_view#set_editable false
-      in
-      let unlock_world _ =
-        main#buttonsToolbar#misc#set_sensitive true;
-        source_view#set_editable true
-      in
+          (source_buffer#get_iter_at_mark (`NAME "locked")) in
       let advance _ = (MatitaScript.instance ())#advance (); cursor () in
       let retract _ = (MatitaScript.instance ())#retract (); cursor () in
       let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
       let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
       let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
-      let locker f = 
-        fun () -> 
-          lock_world ();
-          try f ();unlock_world () with exc -> unlock_world (); raise exc
-      in
-      let advance = locker advance in
-      let retract = locker retract in
-      let top = locker top in
-      let bottom = locker bottom in
-      let jump = locker jump in
+      let advance = locker (keep_focus advance) in
+      let retract = locker (keep_focus retract) in
+      let top = locker (keep_focus top) in
+      let bottom = locker (keep_focus bottom) in
+      let jump = locker (keep_focus jump) in
       let connect_key sym f =
-        connect_key self#main#mainWinEventBox#event
+        connect_key main#mainWinEventBox#event
           ~modifiers:[`CONTROL] ~stop:true sym f;
         connect_key self#sourceView#event
           ~modifiers:[`CONTROL] ~stop:true sym f
@@ -511,19 +690,19 @@ class gui () =
                   GMain.Main.quit ()
                 with MatitaTypes.Cancel -> ())
           end);
-      connect_button self#main#scriptAdvanceButton advance;
-      connect_button self#main#scriptRetractButton retract;
-      connect_button self#main#scriptTopButton top;
-      connect_button self#main#scriptBottomButton bottom;
+      connect_button main#scriptAdvanceButton advance;
+      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 self#main#scriptJumpButton jump;
-      connect_menu_item self#main#openMenuItem   loadScript;
-      connect_menu_item self#main#saveMenuItem   saveScript;
-      connect_menu_item self#main#saveAsMenuItem saveAsScript;
-      connect_menu_item self#main#newMenuItem    newScript;
+      connect_button main#scriptJumpButton 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)
@@ -537,11 +716,11 @@ class gui () =
          (* script monospace font stuff *)  
       self#updateFontSize ();
         (* debug menu *)
-      self#main#debugMenu#misc#hide ();
+      main#debugMenu#misc#hide ();
         (* status bar *)
-      self#main#hintLowImage#set_file (image_path "matita-bulb-low.png");
-      self#main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
-      self#main#hintHighImage#set_file (image_path "matita-bulb-high.png");
+      main#hintLowImage#set_file (image_path "matita-bulb-low.png");
+      main#hintMediumImage#set_file (image_path "matita-bulb-medium.png");
+      main#hintHighImage#set_file (image_path "matita-bulb-high.png");
         (* focus *)
       self#sourceView#misc#grab_focus ();
         (* main win dimension *)
@@ -550,28 +729,64 @@ class gui () =
       let main_w = width * 90 / 100 in 
       let main_h = height * 80 / 100 in
       let script_w = main_w * 6 / 10 in
-      self#main#toplevel#resize ~width:main_w ~height:main_h;
-      self#main#hpaneScriptSequent#set_position script_w;
+      main#toplevel#resize ~width:main_w ~height:main_h;
+      main#hpaneScriptSequent#set_position script_w;
         (* source_view *)
       ignore(source_view#connect#after#paste_clipboard 
-        ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock))
+        ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock));
+      (* clean_locked is set to true only "during" a PRIMARY paste
+         operation (i.e. by clicking with the second mouse button) *)
+      let clean_locked = ref false in
+      ignore(source_view#event#connect#button_press
+        ~callback:
+          (fun button ->
+            if GdkEvent.Button.button button = 2 then
+             clean_locked := true;
+            false
+          ));
+      ignore(source_view#event#connect#button_release
+        ~callback:(fun button -> clean_locked := false; false));
+      ignore(source_view#buffer#connect#after#apply_tag
+       ~callback:(
+         fun tag ~start:_ ~stop:_ ->
+          if !clean_locked &&
+             tag#get_oid = (MatitaScript.instance ())#locked_tag#get_oid
+          then
+           begin
+            clean_locked := false;
+            (MatitaScript.instance ())#clean_dirty_lock;
+            clean_locked := true
+           end));
+      (* math view handling *)
+      connect_menu_item main#newCicBrowserMenuItem (fun () ->
+        ignore (MatitaMathView.cicBrowser ()));
+      connect_menu_item main#increaseFontSizeMenuItem (fun () ->
+        self#increaseFontSize ();
+        MatitaMathView.increase_font_size ();
+        MatitaMathView.update_font_sizes ());
+      connect_menu_item main#decreaseFontSizeMenuItem (fun () ->
+        self#decreaseFontSize ();
+        MatitaMathView.decrease_font_size ();
+        MatitaMathView.update_font_sizes ());
+      connect_menu_item main#normalFontSizeMenuItem (fun () ->
+        self#resetFontSize ();
+        MatitaMathView.reset_font_size ();
+        MatitaMathView.update_font_sizes ());
+      MatitaMathView.reset_font_size ();
     
     method loadScript file =       
       let script = MatitaScript.instance () in
       script#reset (); 
       script#assignFileName file;
-      if not (Sys.file_exists file) then
-        begin
-          let oc = open_out file in
-          let template = MatitaMisc.input_file BuildTimeConf.script_template in 
-          output_string oc template;
-          close_out oc
-        end;
-      source_view#source_buffer#begin_not_undoable_action ();
-      script#loadFromFile ();
-      source_view#source_buffer#end_not_undoable_action ();
-      console#message ("'"^file^"' loaded.");
-      self#_enableSaveTo file
+      let content =
+       if Sys.file_exists file then file
+       else BuildTimeConf.script_template
+      in
+       source_view#source_buffer#begin_not_undoable_action ();
+       script#loadFromFile content;
+       source_view#source_buffer#end_not_undoable_action ();
+       console#message ("'"^file^"' loaded.");
+       self#_enableSaveTo file
       
     method setStar name b =
       let l = main#scriptLabel in
@@ -584,10 +799,9 @@ class gui () =
       script_fname <- Some file;
       self#main#saveMenuItem#misc#set_sensitive true
         
-
     method console = console
-    method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
-    method about = about
+    method sourceView: GSourceView.source_view =
+      (source_view: GSourceView.source_view)
     method fileSel = fileSel
     method findRepl = findRepl
     method main = main
@@ -631,7 +845,7 @@ class gui () =
         keyBindingBoxes
 
     method setQuitCallback callback =
-      ignore (main#quitMenuItem#connect#activate callback);
+      connect_menu_item main#quitMenuItem callback;
       ignore (main#toplevel#event#connect#delete 
         (fun _ -> callback ();true));
       self#addKeyBinding GdkKeysyms._q callback
@@ -695,6 +909,7 @@ class gui () =
 let gui () = 
   let g = new gui () in
   gui_instance := Some g;
+  MatitaMathView.set_gui g;
   g
   
 let instance = singleton gui
@@ -852,3 +1067,12 @@ let interactive_interp_choice () choices =
   GtkThread.main ();
   (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel)
 
+let _ =
+  (* disambiguator callbacks *)
+  MatitaDisambiguator.set_choose_uris_callback (interactive_uri_choice ());
+  MatitaDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
+  (* gtk initialization *)
+  GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
+  GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;
+  ignore (GMain.Main.init ())
+