+let _ =
+ Helm_registry.load_from "matita.conf.xml"; (* read conf *)
+ Http_getter.init ();
+ MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+ MatitaDb.clean_owner_environment ();
+ MatitaDb.create_owner_environment ();
+ GtkMain.Rc.add_default_file BuildTimeConf.gtkrc; (* loads gtk rc files *)
+ ignore (GMain.Main.init ())
+
+let gui = MatitaGui.instance ()
+let _ = (* set disambiguator callbacks *)
+ let disambiguator = MatitaDisambiguator.instance () in
+ disambiguator#setChooseUris (interactive_user_uri_choice ~gui);
+ disambiguator#setChooseInterp (interactive_interp_choice ~gui)
+let _ = (* environment trust *)
+ CicEnvironment.set_trust
+ (let trust = Helm_registry.get_bool "matita.environment_trust" in
+ fun _ -> trust)
+
+let currentProof = MatitaProof.instance ()
+
+
+let sequent_viewer = MatitaMathView.sequent_viewer ~show:true ()
+let sequents_viewer =
+ let set_goal goal =
+ if not (currentProof#onGoing ()) then assert false;
+ currentProof#proof#set_goal goal
+ in
+ MatitaMathView.sequents_viewer ~notebook:gui#main#sequentsNotebook
+ ~sequent_viewer ~set_goal ()
+let _ = (* attach observers to proof status *)
+ let browser_observer _ _ = MatitaMathView.refresh_all_browsers () in
+ let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) =
+ sequents_viewer#reset;
+ (match goal_opt with
+ | None -> ()
+ | Some goal ->
+ sequents_viewer#load_sequents metasenv;
+ sequents_viewer#goto_sequent goal)
+ in
+ currentProof#addObserver sequents_observer;
+ currentProof#addObserver browser_observer;
+ currentProof#connect `Quit (fun () ->
+ (* quit program, asking for confirmation if needed *)
+ if not (currentProof#onGoing ()) ||
+ (ask_confirmation ~gui
+ ~msg:("Proof in progress, are you sure you want to quit?") ())
+ then
+ GMain.Main.quit ();
+ false);
+ currentProof#connect `Abort (fun () -> sequents_viewer#reset; false)