1. Several files in grafite that should be in grafite_parser moved there.

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

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index b901908207b19624ff63346434d33d3fe98c684a..b2c3e9a323070ca26c2c5c2aef159ce52d66ad8c 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -116,7 +116,7 @@ let rec interactive_loop () =
 
 let go () =
   Helm_registry.load_from BuildTimeConf.matita_conf;
-  CicNotation.load_notation BuildTimeConf.core_notation_script;
+  CicNotation2.load_notation BuildTimeConf.core_notation_script;
   Http_getter.init ();
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
   LibraryDb.create_owner_environment ();
@@ -152,12 +152,12 @@ let main ~mode =
       Ulexing.from_utf8_channel
         (match fname with
         | "stdin" -> stdin
-        | fname -> open_in fname)
+        | fname -> open_in fname) in
+    let include_paths =
+     Helm_registry.get_list Helm_registry.string "matita.includes"
     in
     run_script is 
-      (MatitaEngine.eval_from_stream 
-        ~include_paths:(Helm_registry.get_list Helm_registry.string
-          "matita.includes")
+      (MatitaEngine.eval_from_stream ~include_paths
         ~clean_baseuri:(not (Helm_registry.get_bool "matita.preserve")));
     let elapsed = Unix.time () -. time in
     let tm = Unix.gmtime elapsed in
@@ -184,8 +184,9 @@ let main ~mode =
     else
      begin
        let basedir = Helm_registry.get "matita.basedir" in
-       let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in
-       let metadata_fname = GrafiteMisc.metadata_file_of_script ~basedir fname in
+       let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths fname in
+       let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
+       let metadata_fname = LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
        LibraryNoDb.save_metadata metadata_fname metadata;
        HLog.message