New policy for the disambiguation passes.

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

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index ebf1e455bff5d62f4cd9d28f0e0be43441811603..9cc063271d801902cd5375661e5a850458fe9424 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -88,7 +88,7 @@ let fname () =
   Arg.parse arg_spec add_script usage;
   match !acc with
   | [x] -> x
-  | _ -> prerr_endline usage; exit 1
+  | _ -> print_endline usage; exit 1
 
 let pp_ocaml_mode () = 
   MatitaLog.message "";
@@ -134,8 +134,13 @@ let rec interactive_loop () =
 
 let go () =
   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);
   status := Some (ref (Lazy.force MatitaEngine.initial_status));
   Sys.catch_break true;
   interactive_loop ()
@@ -144,7 +149,9 @@ let dump_moo_to_file file moo =
  let os = open_out (MatitaMisc.obj_file_of_script file) in
  let output s = output_string os s in
  output "(* GENERATED FILE: DO NOT EDIT! *)\n\n";
- List.iter output (List.rev moo);
+ List.iter
+  (fun cmd -> output (GrafiteAstPp.pp_command cmd ^ "\n"))
+  (List.rev moo);
  close_out os
   
 let main ~mode = 
@@ -153,6 +160,9 @@ let main ~mode =
   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);
   status := Some (ref (Lazy.force MatitaEngine.initial_status));
   Sys.catch_break true;
   let origcb = MatitaLog.get_log_callback () in