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

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 1bfd5e51e..69bee68a5 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -29,6 +29,9 @@ open MatitaGtkMisc
 open MatitaTypes
 open MatitaMisc
 
+(* ALB to link paramodulation... *)
+let _ = Paramodulation.Saturation.init ()
+
 (** {2 Initialization} *)
 
 let _ =
@@ -38,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)
@@ -48,33 +49,10 @@ 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 
-      ~view:(gui#sourceView :> GText.view)
+      ~source_view:gui#sourceView
       ~init:(Lazy.force MatitaEngine.initial_status) 
       ~mathviewer:(MatitaMathView.mathViewer ())
       ~urichooser:(fun uris ->
@@ -100,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;
@@ -147,13 +125,13 @@ let _ =
         prerr_endline (UriManager.string_of_uri u); 
         CicUniv.print_ugraph g) (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);
+    addDebugItem "dump environment content" (fun _ ->
+      List.iter (fun (u,_,_) -> 
+        prerr_endline (UriManager.string_of_uri u)) 
+        (CicEnvironment.list_obj ()));
+    addDebugItem "print selections" (fun () ->
+      let sequentViewer = MatitaMathView.sequentViewer_instance () in
+      List.iter MatitaLog.debug (sequentViewer#string_of_selections));
     addDebugItem "dump getter settings" (fun _ ->
       prerr_endline (Http_getter_env.env_to_string ()));
     addDebugItem "getter: getalluris" (fun _ ->
@@ -181,9 +159,6 @@ let _ =
 let _ =
   at_exit (fun () -> print_endline "\nThanks for using Matita!\n");
   Sys.catch_break true;
-  (try
-     gui#loadScript Sys.argv.(1);
-   with Invalid_argument _ -> ());
   if Filename.basename Sys.argv.(0) = "cicbrowser" then begin (* cicbrowser *)
     Helm_registry.set "matita.mode" "cicbrowser";
     let browser = MatitaMathView.cicBrowser () in
@@ -195,6 +170,9 @@ let _ =
     browser#load entry
   end else begin  (* matita *)
     Helm_registry.set "matita.mode" "matita";
+    (try
+       gui#loadScript Sys.argv.(1);
+     with Invalid_argument _ -> ());
     gui#main#mainWin#show ();
   end;
   try