X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Fmatita.ml;h=aae334abd56e79927c748b3636c02a3160222468;hb=cec61c8b027b15b98d308cee8900d9cf35a02d28;hp=3eb0fc6a15f985c897e07144b0949c41688805d7;hpb=6fa3a1e91d8a1e647775ca101255633ba265a9f2;p=helm.git

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 3eb0fc6a1..aae334abd 100644
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -29,19 +29,25 @@ open MatitaGtkMisc
 open MatitaTypes
 open MatitaMisc
 
+
+(* ALB to link paramodulation... *)
+let _ = Paramodulation.Saturation.init ()
+  
+
 (** {2 Initialization} *)
 
 let _ =
-  Helm_registry.load_from "matita.conf.xml";  (* read conf *)
+  Helm_registry.load_from BuildTimeConf.matita_conf;
+  CicNotation.load_notation BuildTimeConf.core_notation_script;
   Http_getter.init ();
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
-(*  MatitaDb.clean_owner_environment ();
-  MatitaDb.create_owner_environment (); *)
+  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 ());
-
-  (* environment trust *)
-  CicEnvironment.set_trust
+  CicEnvironment.set_trust (* environment trust *)
     (let trust = Helm_registry.get_bool "matita.environment_trust" in
      fun _ -> trust)
 
@@ -73,25 +79,34 @@ let _ =
     (MatitaGui.interactive_interp_choice ())
 
 let script =
-  MatitaScript.script 
-    ~buffer:gui#sourceView#buffer
-    ~init:(Lazy.force MatitaEngine.initial_status) 
-    ~mathviewer:(MatitaMathView.mathViewer ())
-    ~urichooser:(fun uris ->
-      try
-        MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
-        ~title:"Matita: URI chooser" 
-        ~msg:"Select the URI" ~hide_uri_entry:true
-        ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
-        ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
-        () ~id:"boh?" uris
-      with MatitaTypes.Cancel -> [])
-    ~set_star:gui#setStar
-    ~ask_confirmation:
-      (fun ~title ~message -> 
-          MatitaGtkMisc.ask_confirmation ~title ~message 
-          ~parent:gui#main#toplevel ())
-    ()
+  let s = 
+    MatitaScript.script 
+      ~view:(gui#sourceView :> GText.view)
+      ~init:(Lazy.force MatitaEngine.initial_status) 
+      ~mathviewer:(MatitaMathView.mathViewer ())
+      ~urichooser:(fun uris ->
+        try
+          MatitaGui.interactive_uri_choice ~selection_mode:`SINGLE
+          ~title:"Matita: URI chooser" 
+          ~msg:"Select the URI" ~hide_uri_entry:true
+          ~hide_try:true ~ok_label:"_Apply" ~ok_action:`SELECT
+          ~copy_cb:(fun s -> gui#sourceView#buffer#insert ("\n"^s^"\n"))
+          () ~id:"boh?" uris
+        with MatitaTypes.Cancel -> [])
+      ~set_star:gui#setStar
+      ~ask_confirmation:
+        (fun ~title ~message -> 
+            MatitaGtkMisc.ask_confirmation ~title ~message 
+            ~parent:gui#main#toplevel ())
+      ~develcreator:gui#createDevelopment
+      ()
+  in
+  gui#sourceView#source_buffer#begin_not_undoable_action ();
+  s#reset (); 
+  s#template (); 
+  gui#sourceView#source_buffer#end_not_undoable_action ();
+  s
+  
 
   (* math viewers *)
 let _ =
@@ -139,6 +154,10 @@ let _ =
         prerr_endline (UriManager.string_of_uri u); 
         CicUniv.print_ugraph g) (CicEnvironment.list_obj ())
       );
+    addDebugItem "dump environment content" (fun _ ->
+      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
@@ -148,12 +167,6 @@ let _ =
         (MatitaMathView.sequentViewer_instance ())#get_selected_terms);
     addDebugItem "dump getter settings" (fun _ ->
       prerr_endline (Http_getter_env.env_to_string ()));
-    addDebugItem "getter: update"
-      (fun _ ->
-         ignore (Thread.create (fun () ->
-           MatitaLog.message "Rebuilding getter maps in background ...";
-           Http_getter.update ();
-           MatitaLog.message "Getter maps successfully rebuilt.") ()));
     addDebugItem "getter: getalluris" (fun _ ->
       List.iter prerr_endline (Http_getter.getalluris ()));
     addDebugItem "dump script status" script#dump;
@@ -162,37 +175,23 @@ let _ =
          if script#onGoingProof () then
            MatitaLog.debug (CicMetaSubst.ppmetasenv script#proofMetasenv []));
     addDebugItem "dump coercions Db" (fun _ ->
-      List.iter (
-        fun (s,t,u) -> 
-          MatitaLog.debug (
-            UriManager.name_of_uri u ^ ":" ^ 
-            UriManager.name_of_uri s ^ " -> " ^ UriManager.name_of_uri t))
-      (CoercDb.to_list ())
-    );
+      List.iter
+        (fun (s,t,u) -> 
+          MatitaLog.debug
+            (UriManager.name_of_uri u ^ ":"
+             ^ UriManager.name_of_uri s ^ " -> " ^ UriManager.name_of_uri t))
+        (CoercDb.to_list ()));
     addDebugItem "rotate light bulbs"
       (fun _ ->
          let nb = gui#main#hintNotebook in
-         nb#goto_page ((nb#current_page + 1) mod 3));
-         (*
-    addDebugItem "print (on stdout) \"statement\" grammar entry"
-      (fun _ ->
-        Grammar.print_entry Format.std_formatter
-          (Grammar.Entry.obj CicTextualParser2.statement);
-        Format.pp_print_flush Format.std_formatter ());*)
+         nb#goto_page ((nb#current_page + 1) mod 3))
   end
 
   (** </DEBUGGING> *)
 
 let _ =
-  at_exit
-    (fun () ->
-       Http_getter_logger.log "Sync map tree to disk...";
-       Http_getter.sync_dump_file ();
-       print_endline "\nThanks for using Matita!\n");
+  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
@@ -204,6 +203,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