From 3ce38077e0b1e2a38ad513d3c108d7ef3c09bb7c Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 3 Dec 2005 10:35:32 +0000
Subject: [PATCH] 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"

---
 helm/matita/dump_moo.ml     | 6 +-----
 helm/matita/matita.ml       | 6 ++----
 helm/matita/matitaEngine.ml | 3 ++-
 helm/matita/matitaGui.ml    | 6 ++++--
 helm/matita/matitacLib.ml   | 6 ++++--
 5 files changed, 13 insertions(+), 14 deletions(-)

diff --git a/helm/matita/dump_moo.ml b/helm/matita/dump_moo.ml
index cf872bdeb..17f24fc0a 100644
--- 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 0a83b737e..769f294fd 100644
--- 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 e682adfcc..c0f74962d 100644
--- 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 6b4afa3cf..74913dbe6 100644
--- 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 55c5f2a02..b90190820 100644
--- 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
-- 
2.39.2