X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.ml;h=fbf3d500e07fa93736e8088480f340bc05a64183;hb=ddff8ae1e15c9fcaf83320978a5cad509d734a74;hp=d0223a80bccf8e0b7f7cb1ff8a7bb430dcf95051;hpb=786d6e21b707035b6fb60353cef09fb8a17a58ac;p=helm.git

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index d0223a80b..fbf3d500e 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -29,10 +29,8 @@ open MatitaGtkMisc
 open MatitaTypes
 open MatitaMisc
 
-
 (* ALB to link paramodulation... *)
-let _ = Saturation.init ()
-  
+let _ = Paramodulation.Saturation.init ()
 
 (** {2 Initialization} *)
 
@@ -43,8 +41,6 @@ let _ =
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
   MatitaDb.create_owner_environment ();
   MatitamakeLib.initialize ();
-  GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
-  ignore (GMain.Main.init ());
   CicEnvironment.set_trust (* environment trust *)
     (let trust = Helm_registry.get_bool "matita.environment_trust" in
      fun _ -> trust)
@@ -53,29 +49,6 @@ let _ =
 
 let gui = MatitaGui.instance ()
 
-let _ =
-  ignore (gui#main#newCicBrowserMenuItem#connect#activate (fun _ ->
-    ignore (MatitaMathView.cicBrowser ())));
-  (* font sizes *)
-  ignore (gui#main#increaseFontSizeMenuItem#connect#activate (fun _ ->
-    gui#increaseFontSize ();
-    MatitaMathView.increase_font_size ();
-    MatitaMathView.update_font_sizes ()));
-  ignore (gui#main#decreaseFontSizeMenuItem#connect#activate (fun _ ->
-    gui#decreaseFontSize ();
-    MatitaMathView.decrease_font_size ();
-    MatitaMathView.update_font_sizes ()));
-  ignore (gui#main#normalFontSizeMenuItem#connect#activate (fun _ ->
-    gui#resetFontSize ();
-    MatitaMathView.reset_font_size ();
-    MatitaMathView.update_font_sizes ()));
-  MatitaMathView.reset_font_size ();
-  (* disambiguator callback *)
-  MatitaDisambiguator.set_choose_uris_callback
-    (MatitaGui.interactive_uri_choice ());
-  MatitaDisambiguator.set_choose_interp_callback
-    (MatitaGui.interactive_interp_choice ())
-
 let script =
   let s = 
     MatitaScript.script 
@@ -105,13 +78,13 @@ let script =
   gui#sourceView#source_buffer#end_not_undoable_action ();
   s
   
-
   (* math viewers *)
 let _ =
   let sequent_viewer = MatitaMathView.sequentViewer_instance () in
   let sequents_viewer = MatitaMathView.sequentsViewer_instance () in
   sequent_viewer#set_href_callback
-    (Some (fun uri -> (MatitaMathView.cicBrowser ())#load (`Uri (UriManager.uri_of_string uri))));
+    (Some (fun uri -> (MatitaMathView.cicBrowser ())#load
+      (`Uri (UriManager.uri_of_string uri))));
   let browser_observer _ = MatitaMathView.refresh_all_browsers () in
   let sequents_observer status =
     sequents_viewer#reset;
@@ -157,12 +130,8 @@ let _ =
         prerr_endline (UriManager.string_of_uri u)) 
         (CicEnvironment.list_obj ()));
     addDebugItem "print selected terms" (fun () ->
-      let i = ref 0 in
-      List.iter
-        (fun t ->
-           incr i;
-           MatitaLog.debug (sprintf "%d: %s" !i (CicPp.ppterm t)))
-        (MatitaMathView.sequentViewer_instance ())#get_selected_terms);
+      let sequentViewer = MatitaMathView.sequentViewer_instance () in
+      MatitaLog.debug (sequentViewer#string_of_selected_terms));
     addDebugItem "dump getter settings" (fun _ ->
       prerr_endline (Http_getter_env.env_to_string ()));
     addDebugItem "getter: getalluris" (fun _ ->