]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitacLib.ml
log.ma renamed into ord.ma
[helm.git] / helm / matita / matitacLib.ml
index a795f5f4b6eef94dc0dbafd8bf71306850c3239d..b30a55234b94f12d80c6330eefac65bba5de2636 100644 (file)
@@ -127,7 +127,7 @@ let clean_exit n =
        opt_exit n
   
 let rec interactive_loop () = 
let str = Stream.of_channel stdin in
 let str = Ulexing.from_utf8_channel stdin in
   try
     run_script str 
       (MatitaEngine.eval_from_stream_greedy ~include_paths:!paths_to_search_in)
@@ -167,14 +167,7 @@ let dump_moo_to_file file moo =
  close_out os
   
 let main ~mode = 
-  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 ();
-  CicEnvironment.set_trust (* environment trust *)
-    (let trust = Helm_registry.get_bool "matita.environment_trust" in
-     fun _ -> trust);
+  MatitaInit.initialize_all ();
   status := Some (ref (Lazy.force MatitaEngine.initial_status));
   Sys.catch_break true;
   let origcb = MatitaLog.get_log_callback () in
@@ -193,7 +186,7 @@ let main ~mode =
     else
       MatitaLog.message (sprintf "execution of %s started:" fname);
     let is =
-      Stream.of_channel
+      Ulexing.from_utf8_channel
         (match fname with
         | "stdin" -> stdin
         | fname -> open_in fname)