fixed a finalization issue for connections closed twice

[helm.git] / helm / matita / matita.ml

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index d4f9c3fac85bd102e472bc2a9e06648b20b65e4a..2a87554d8f76bb2bf405e3b46e6ec8a539cd6263 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -29,11 +29,6 @@ open MatitaGtkMisc
 open MatitaTypes
 open MatitaMisc
 
-
-(* ALB to link paramodulation... *)
-let _ = Paramodulation.Saturation.init ()
-  
-
 (** {2 Initialization} *)
 
 let _ =
@@ -43,43 +38,19 @@ 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)
+     fun _ -> trust);
+  Paramodulation.Saturation.init ()
 
 (** {2 GUI callbacks} *)
 
 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 ->
@@ -105,13 +76,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;
@@ -119,12 +91,9 @@ let _ =
     | Incomplete_proof ((proof, goal) as status) ->
         sequents_viewer#load_sequents status;
         sequents_viewer#goto_sequent goal
-    | Proof proof -> 
-        prerr_endline "sequents_viewer#load_logo_with_qed (no proof)"; ()
-    | No_proof -> 
-        prerr_endline "sequents_viewer#load_logo (no proof)"; ()
-    | Intermediate _ -> 
-        assert false (* only the engine may be in this state *)
+    | Proof proof -> sequents_viewer#load_logo_with_qed
+    | No_proof -> sequents_viewer#load_logo
+    | Intermediate _ -> assert false (* only the engine may be in this state *)
   in
   script#addObserver sequents_observer;
   script#addObserver browser_observer
@@ -156,13 +125,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 _ ->
@@ -179,10 +144,16 @@ let _ =
             (UriManager.name_of_uri u ^ ":"
              ^ UriManager.name_of_uri s ^ " -> " ^ UriManager.name_of_uri t))
         (CoercDb.to_list ()));
+    addDebugItem "print top-level grammar entries"
+      CicNotationParser.print_l2_pattern;
+    addDebugItem "dump moo to stderr" (fun _ ->
+      let status = (MatitaScript.instance ())#status in
+      List.iter (fun cmd -> prerr_endline
+        (GrafiteAstPp.pp_command cmd)) (List.rev status.moo_content_rev));
     addDebugItem "rotate light bulbs"
       (fun _ ->
          let nb = gui#main#hintNotebook in
-         nb#goto_page ((nb#current_page + 1) mod 3))
+         nb#goto_page ((nb#current_page + 1) mod 3));
   end
 
   (** </DEBUGGING> *)