X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.ml;h=0066d1c1816fcc5d3a7ab8ea142d1eef1744ba4f;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=aae334abd56e79927c748b3636c02a3160222468;hpb=13fab17e3d3dee05df676985c065ae54a5766870;p=helm.git

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index aae334abd..0066d1c18 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 _ = Paramodulation.Saturation.init ()
-  
 
 (** {2 Initialization} *)
 
@@ -43,10 +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 *)
-  prerr_endline BuildTimeConf.gtkmathview_conf;
-  GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;
-  ignore (GMain.Main.init ());
   CicEnvironment.set_trust (* environment trust *)
     (let trust = Helm_registry.get_bool "matita.environment_trust" in
      fun _ -> trust)
@@ -55,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 ->
@@ -107,13 +78,14 @@ let script =
   gui#sourceView#source_buffer#end_not_undoable_action ();
   s
   
-
   (* math viewers *)
 let _ =
-  let sequent_viewer = MatitaMathView.sequentViewer_instance () in
+  let cic_math_view = MatitaMathView.cicMathView_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))));
+  sequents_viewer#load_logo;
+  cic_math_view#set_href_callback
+    (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;
@@ -122,9 +94,9 @@ let _ =
         sequents_viewer#load_sequents status;
         sequents_viewer#goto_sequent goal
     | Proof proof -> 
-        prerr_endline "sequents_viewer#load_logo_with_qed (no proof)"; ()
+        sequents_viewer#load_logo_with_qed
     | No_proof -> 
-        prerr_endline "sequents_viewer#load_logo (no proof)"; ()
+        sequents_viewer#load_logo
     | Intermediate _ -> 
         assert false (* only the engine may be in this state *)
   in
@@ -158,13 +130,9 @@ let _ =
       List.iter (fun (u,_,_) -> 
         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);
+    addDebugItem "print selections" (fun () ->
+      let cicMathView = MatitaMathView.cicMathView_instance () in
+      List.iter MatitaLog.debug (cicMathView#string_of_selections));
     addDebugItem "dump getter settings" (fun _ ->
       prerr_endline (Http_getter_env.env_to_string ()));
     addDebugItem "getter: getalluris" (fun _ ->