metadata are no longer stored in .moo files.

They are now stored (and retrieved) in .metadata files if -nodb is set.
In this way the "library" library no longer depends on "content_pres"

diff --git a/helm/matita/dump_moo.ml b/helm/matita/dump_moo.ml
index cf872bdebcd4c02e812b294a716c1105cd171aa7..17f24fc0afb3da92e73f70645b73d9fda9ad4dd8 100644 (file)
--- a/helm/matita/dump_moo.ml
+++ b/helm/matita/dump_moo.ml
@@ -45,15 +45,11 @@ let _ =
         HLog.error (sprintf "Can't find moo '%s', skipping it." fname)
       else begin
         printf "%s:\n" fname; flush stdout;
-        let commands, metadata = GrafiteMarshal.load_moo ~fname in
+        let commands = GrafiteMarshal.load_moo ~fname in
         List.iter
           (fun cmd ->
             printf "  %s\n" (GrafiteAstPp.pp_cic_command cmd); flush stdout)
           commands;
-        List.iter
-          (fun m ->
-            printf "  %s\n" (GrafiteAstPp.pp_metadata m); flush stdout)
-          metadata
       end)
     (List.rev !moos)
 

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 0a83b737ebe54e7ee4dd7db23c9bd1eb824bd0e1..769f294fd2ef6d2743ef4d925bee4c3191afb3c2 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -139,11 +139,9 @@ let _ =
       CicNotationParser.print_l2_pattern;
     addDebugItem "dump moo to stderr" (fun _ ->
       let status = (MatitaScript.current ())#status in
-      let moo, metadata = status.moo_content_rev in
+      let moo = status.moo_content_rev in
       List.iter (fun cmd -> prerr_endline
-        (GrafiteAstPp.pp_cic_command cmd)) (List.rev moo);
-      List.iter (fun m -> prerr_endline
-        (GrafiteAstPp.pp_metadata m)) metadata);
+        (GrafiteAstPp.pp_cic_command cmd)) (List.rev moo));
     addDebugItem "print metasenv goals and stack to stderr"
       (fun _ ->
         prerr_endline ("metasenv goals: " ^ String.concat " "

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index e682adfcc6da7ee9351513ea08a0dd40b28940a2..c0f74962da394fd73325f75e869f637f45321603 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -72,7 +72,8 @@ let initial_status =
   lazy {
     aliases = DisambiguateTypes.Environment.empty;
     multi_aliases = DisambiguateTypes.Environment.empty;
-    moo_content_rev = [], [];
+    moo_content_rev = [];
+    metadata = [];
     proof_status = No_proof;
     options = default_options ();
     objects = [];

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 6b4afa3cf3e549f9f484ed54c71d14504750965e..74913dbe6d46c596cc73ecb640e93ac218c27e28 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -72,8 +72,10 @@ let ask_and_save_moo_if_needed parent fname status =
   let basedir = Helm_registry.get "matita.basedir" in
   let save () =
     let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in
-     GrafiteMarshal.save_moo moo_fname
-      status.GrafiteTypes.moo_content_rev in
+    let metadata_fname = GrafiteMisc.metadata_file_of_script ~basedir fname in
+    GrafiteMarshal.save_moo moo_fname status.GrafiteTypes.moo_content_rev;
+    LibraryNoDb.save_metadata metadata_fname status.GrafiteTypes.metadata
+  in
   if (MatitaScript.current ())#eos &&
      status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
   then

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 55c5f2a02318f66b9f66601a882cc3e41e9141bc..b901908207b19624ff63346434d33d3fe98c684a 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -170,9 +170,9 @@ let main ~mode =
     let hou = 
       if tm.Unix.tm_hour > 0 then (string_of_int tm.Unix.tm_hour ^ "h ") else ""
     in
-    let proof_status,moo_content_rev,status = 
+    let proof_status,moo_content_rev,metadata,status = 
       match !status with
-      | Some s -> !s.proof_status, !s.moo_content_rev, !s
+      | Some s -> !s.proof_status, !s.moo_content_rev, !s.metadata, !s
       | None -> assert false
     in
     if proof_status <> GrafiteTypes.No_proof then
@@ -185,7 +185,9 @@ let main ~mode =
      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
        GrafiteMarshal.save_moo moo_fname moo_content_rev;
+       LibraryNoDb.save_metadata metadata_fname metadata;
        HLog.message 
          (sprintf "execution of %s completed in %s." fname (hou^min^sec));
        exit 0