X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fmatita.ml;h=db0fd2b18e7ec0be350aecbea58d29dc16745933;hb=ad0292419b0204384ff55c946a6aabb73a47c42b;hp=ade151a6900d28e0c395d6a44cb329d5442fc853;hpb=be4d6187ed0970df4b6285ee642d98ec1833a6fe;p=helm.git diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index ade151a69..db0fd2b18 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -33,14 +33,14 @@ open MatitaMisc let _ = 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.create_owner_environment (); + MatitamakeLib.initialize (); GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) 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,7 +73,7 @@ let _ = let script = MatitaScript.script - ~buffer:gui#sourceView#buffer + ~view:(gui#sourceView :> GText.view) ~init:(Lazy.force MatitaEngine.initial_status) ~mathviewer:(MatitaMathView.mathViewer ()) ~urichooser:(fun uris -> @@ -90,6 +90,7 @@ let script = (fun ~title ~message -> MatitaGtkMisc.ask_confirmation ~title ~message ~parent:gui#main#toplevel ()) + ~develcreator:gui#createDevelopment () (* math viewers *) @@ -155,23 +156,16 @@ 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 (** *)